---

Step * 3 of Lemma translation-group_wf


1. rv : InnerProductSpace
2. e : Point
3. T : ℝ ⟶ Point ⟶ Point
4. translation-group-fun(rv;e;T)
5. ∀fg:Point. ((∃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))
6. 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))} 
7. y : {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))} 
8. ∃t:ℝ. ∀x@0:Point. (fst(fg)) x@0 ≡ T t x@0
9. ∃t:ℝ. ∀x@0:Point. (fst(y)) x@0 ≡ T t x@0
⊢ ∃t:ℝ. ∀x@0:Point. (fst((fg y))) x@0 ≡ T t x@0
BY
{ (DupHyp 4
   THEN PromoteHyp (-1) 4
   THEN D 4
   THEN (RWO "rv-perm-op" 0 THENA Auto)
   THEN ExRepD
   THEN All (Fold `trans-apply`)
   THEN D 0 With ⌜t1 + t⌝ 
   THEN Auto
   THEN (RepeatFor 2 (DVar `fg') THEN RepeatFor 2 (DVar `y'))
   THEN Reduce 0
   THEN All Reduce
   THEN RWW "-4 -2 5" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  e  :  Point
3.  T  :  \mBbbR{}  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point
4.  translation-group-fun(rv;e;T)
5.  \mforall{}fg:Point
          ((\mexists{}t:\mBbbR{}.  \mforall{}x@0:Point.  (fst(fg))  x@0  \mequiv{}  T  t  x@0)  {}\mRightarrow{}  (\mexists{}t:\mBbbR{}.  \mforall{}x@0:Point.  (fst(fg\^{}-1))  x@0  \mequiv{}  T  t  x@0))
6.  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))\} 
7.  y  :  \{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))\} 
8.  \mexists{}t:\mBbbR{}.  \mforall{}x@0:Point.  (fst(fg))  x@0  \mequiv{}  T  t  x@0
9.  \mexists{}t:\mBbbR{}.  \mforall{}x@0:Point.  (fst(y))  x@0  \mequiv{}  T  t  x@0
\mvdash{}  \mexists{}t:\mBbbR{}.  \mforall{}x@0:Point.  (fst((fg  y)))  x@0  \mequiv{}  T  t  x@0


By

---

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

---

Home Index