Step
*
1
of Lemma
translation-group-point
1. rv : InnerProductSpace
2. e : Point
3. T : ℝ ⟶ Point ⟶ Point
4. translation-group-fun(rv;e;T)
5. x1 : Point ⟶ Point
6. x2 : Point ⟶ Point
7. ∀x:Point. x1 (x2 x) ≡ x
8. ∀x:Point. x2 (x1 x) ≡ x
9. ∀x,y:Point. (x1 x # x1 y
⇒ x # y)
10. ∀x,y:Point. (x2 x # x2 y
⇒ x # y)
11. t : ℝ
12. ∀x@0:Point. x1 x@0 ≡ T t x@0
13. ∀x:Point. x1 x ≡ T t x
14. x : Point
⊢ x2 x ≡ T -(t) x
BY
{ ((Assert T_-(t)(x1 (x2 x)) ≡ T_-(t)(x) BY
(RWO "7" 0 THEN Auto))
THEN Fold `trans-apply` (-3)
THEN (RWO "-3" (-1) THENA Auto)) }
1
1. rv : InnerProductSpace
2. e : Point
3. T : ℝ ⟶ Point ⟶ Point
4. translation-group-fun(rv;e;T)
5. x1 : Point ⟶ Point
6. x2 : Point ⟶ Point
7. ∀x:Point. x1 (x2 x) ≡ x
8. ∀x:Point. x2 (x1 x) ≡ x
9. ∀x,y:Point. (x1 x # x1 y
⇒ x # y)
10. ∀x,y:Point. (x2 x # x2 y
⇒ x # y)
11. t : ℝ
12. ∀x@0:Point. x1 x@0 ≡ T t x@0
13. ∀x:Point. x1 x ≡ T_t(x)
14. x : Point
15. T_-(t)(T_t(x2 x)) ≡ T_-(t)(x)
⊢ x2 x ≡ T -(t) x
Latex:
Latex:
1. rv : InnerProductSpace
2. e : Point
3. T : \mBbbR{} {}\mrightarrow{} Point {}\mrightarrow{} Point
4. translation-group-fun(rv;e;T)
5. x1 : Point {}\mrightarrow{} Point
6. x2 : Point {}\mrightarrow{} Point
7. \mforall{}x:Point. x1 (x2 x) \mequiv{} x
8. \mforall{}x:Point. x2 (x1 x) \mequiv{} x
9. \mforall{}x,y:Point. (x1 x \# x1 y {}\mRightarrow{} x \# y)
10. \mforall{}x,y:Point. (x2 x \# x2 y {}\mRightarrow{} x \# y)
11. t : \mBbbR{}
12. \mforall{}x@0:Point. x1 x@0 \mequiv{} T t x@0
13. \mforall{}x:Point. x1 x \mequiv{} T t x
14. x : Point
\mvdash{} x2 x \mequiv{} T -(t) x
By
Latex:
((Assert T\_-(t)(x1 (x2 x)) \mequiv{} T\_-(t)(x) BY
(RWO "7" 0 THEN Auto))
THEN Fold `trans-apply` (-3)
THEN (RWO "-3" (-1) THENA Auto))
Home
Index