---

Step * of Lemma translation-group-point

∀rv:InnerProductSpace. ∀e:Point. ∀T:ℝ ⟶ Point ⟶ Point.
  (translation-group-fun(rv;e;T)
  ⇒ Point ≡ {fg:Point ⟶ Point × (Point ⟶ Point)| 
              ∃t:ℝ. ((∀x:Point. (fst(fg)) x ≡ T t x) ∧ (∀x:Point. (snd(fg)) x ≡ T -(t) x))} )
BY
{ ((UnivCD THENA Auto)
   THEN (Subst' Point ~ {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))} | 
                         ∃t:ℝ. ∀x:Point. (fst(fg)) x ≡ T t x}  0
         THENA (RepUR ``ss-point translation-group mk-s-subgroup mk-s-group`` 0
                THEN RepUR ``set-ss mk-ss`` 0
                THEN (RWO "rv-perm-point" 0 THENA Auto)
                THEN Fold `ss-point` 0
                THEN Auto)
         )
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN Repeat (DSetVars)
   THEN DVar `x'
   THEN All Reduce
   THEN Repeat ((MemTypeCD THENW Auto))
   THEN ((MemCD THEN Trivial) ORELSE (Reduce 0 THEN Try ((ParallelLast THEN 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
⊢ x2 x ≡ T -(t) x

2
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. ∃t:ℝ. ((∀x@0:Point. x1 x@0 ≡ T t x@0) ∧ (∀x@0:Point. x2 x@0 ≡ T -(t) x@0))
⊢ (∀x:Point. x1 (x2 x) ≡ x)
∧ (∀x:Point. x2 (x1 x) ≡ x)
∧ (∀x,y:Point.  (x1 x # x1 y ⇒ x # y))
∧ (∀x,y:Point.  (x2 x # x2 y ⇒ x # y))

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}e:Point.  \mforall{}T:\mBbbR{}  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point.
    (translation-group-fun(rv;e;T)
    {}\mRightarrow{}  Point  \mequiv{}  \{fg:Point  {}\mrightarrow{}  Point  \mtimes{}  (Point  {}\mrightarrow{}  Point)| 
                            \mexists{}t:\mBbbR{}.  ((\mforall{}x:Point.  (fst(fg))  x  \mequiv{}  T  t  x)  \mwedge{}  (\mforall{}x:Point.  (snd(fg))  x  \mequiv{}  T  -(t)  x))\}  )


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Subst'  Point  \msim{}  \{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))\}  | 
                                              \mexists{}t:\mBbbR{}.  \mforall{}x:Point.  (fst(fg))  x  \mequiv{}  T  t  x\}    0
              THENA  (RepUR  ``ss-point  translation-group  mk-s-subgroup  mk-s-group``  0
                            THEN  RepUR  ``set-ss  mk-ss``  0
                            THEN  (RWO  "rv-perm-point"  0  THENA  Auto)
                            THEN  Fold  `ss-point`  0
                            THEN  Auto)
              )
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  Repeat  (DSetVars)
  THEN  DVar  `x'
  THEN  All  Reduce
  THEN  Repeat  ((MemTypeCD  THENW  Auto))
  THEN  ((MemCD  THEN  Trivial)  ORELSE  (Reduce  0  THEN  Try  ((ParallelLast  THEN  Auto)))))

---

Home Index