---

Step * 2 of Lemma translation-group_wf


1. rv : InnerProductSpace
2. e : Point
3. T : ℝ ⟶ Point ⟶ Point
4. translation-group-fun(rv;e;T)
5. fg : {fg:Point ⟶ Point × (Point ⟶ Point)| 
         let f,g = fg 
         in (∀x:Point. f (g x) ≡ x)
            ∧ (∀x:Point. g (f x) ≡ x)
            ∧ (∀x,y:Point.  (f x # f y ⇒ x # y))
            ∧ (∀x,y:Point.  (g x # g y ⇒ x # y))} 
6. ∃t:ℝ. ∀x@0:Point. (fst(fg)) x@0 ≡ T t x@0
⊢ ∃t:ℝ. ∀x@0:Point. (fst(fg^-1)) x@0 ≡ T t x@0
BY
{ (DupHyp 4
   THEN PromoteHyp (-1) 4
   THEN D 4
   THEN (RWO "rv-perm-inv" 0 THENA Auto)
   THEN ExRepD
   THEN All (Fold `trans-apply`)
   THEN D 0 With ⌜-(t)⌝ 
   THEN Auto
   THEN RepeatFor 2 (DVar `fg')
   THEN All Reduce
   THEN Unhide
   THEN Auto) }

1
1. rv : InnerProductSpace
2. e : Point
3. T : ℝ ⟶ Point ⟶ Point
4. ∀s,t:ℝ. ∀x,y:Point.  (T_s(x) # T_t(y) ⇒ (x # y ∨ s ≠ t))
5. ∀t,s:ℝ. ∀x:Point.  T_t + s(x) ≡ T_t(T_s(x))
6. ∀x:Point. ∀r:ℝ.  ∃t:ℝ. (T_t(x) ≡ x + r*e ∧ (∀y:ℝ. (T_y(x) ≡ x + r*e ⇒ (y = t))))
7. ∀x:Point. ∀t:{t:ℝ| r0 ≤ t} .  ∃r:{t:ℝ| r0 ≤ t} . T_t(x) ≡ x + r*e
8. translation-group-fun(rv;e;T)
9. f1 : Point ⟶ Point
10. f2 : Point ⟶ Point
11. ∀x:Point. f1 (f2 x) ≡ x
12. ∀x:Point. f2 (f1 x) ≡ x
13. ∀x,y:Point.  (f1 x # f1 y ⇒ x # y)
14. ∀x,y:Point.  (f2 x # f2 y ⇒ x # y)
15. t : ℝ
16. ∀x@0:Point. f1 x@0 ≡ T_t(x@0)
17. x@0 : Point
⊢ f2 x@0 ≡ T_-(t)(x@0)

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  e  :  Point
3.  T  :  \mBbbR{}  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point
4.  translation-group-fun(rv;e;T)
5.  fg  :  \{fg:Point  {}\mrightarrow{}  Point  \mtimes{}  (Point  {}\mrightarrow{}  Point)| 
                  let  f,g  =  fg 
                  in  (\mforall{}x:Point.  f  (g  x)  \mequiv{}  x)
                        \mwedge{}  (\mforall{}x:Point.  g  (f  x)  \mequiv{}  x)
                        \mwedge{}  (\mforall{}x,y:Point.    (f  x  \#  f  y  {}\mRightarrow{}  x  \#  y))
                        \mwedge{}  (\mforall{}x,y:Point.    (g  x  \#  g  y  {}\mRightarrow{}  x  \#  y))\} 
6.  \mexists{}t:\mBbbR{}.  \mforall{}x@0:Point.  (fst(fg))  x@0  \mequiv{}  T  t  x@0
\mvdash{}  \mexists{}t:\mBbbR{}.  \mforall{}x@0:Point.  (fst(fg\^{}-1))  x@0  \mequiv{}  T  t  x@0


By

---

Latex:
(DupHyp  4
  THEN  PromoteHyp  (-1)  4
  THEN  D  4
  THEN  (RWO  "rv-perm-inv"  0  THENA  Auto)
  THEN  ExRepD
  THEN  All  (Fold  `trans-apply`)
  THEN  D  0  With  \mkleeneopen{}-(t)\mkleeneclose{} 
  THEN  Auto
  THEN  RepeatFor  2  (DVar  `fg')
  THEN  All  Reduce
  THEN  Unhide
  THEN  Auto)

---

Home Index