---

Step * of Lemma translation-group_wf

∀rv:InnerProductSpace. ∀e:Point. ∀T:ℝ ⟶ Point ⟶ Point.
  translation-group(rv;e;T) ∈ s-Group supposing translation-group-fun(rv;e;T)
BY
{ (ProveWfLemma
   THEN Try ((OnVar `fg' (RWO "rv-perm-point")⋅ THEN Auto))
   THEN D 0
   THEN Auto
   THEN Try ((OnVar `fg' (RWO "rv-perm-point")⋅ THEN Auto))
   THEN Try ((OnVar `y' (RWO "rv-perm-point")⋅ THEN Auto))) }

1
1. rv : InnerProductSpace
2. e : Point
3. T : ℝ ⟶ Point ⟶ Point
4. translation-group-fun(rv;e;T)
⊢ ∃t:ℝ. ∀x@0:Point. (fst(1)) x@0 ≡ T t x@0

2
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

3
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

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}e:Point.  \mforall{}T:\mBbbR{}  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point.
    translation-group(rv;e;T)  \mmember{}  s-Group  supposing  translation-group-fun(rv;e;T)


By

---

Latex:
(ProveWfLemma
  THEN  Try  ((OnVar  `fg'  (RWO  "rv-perm-point")\mcdot{}  THEN  Auto))
  THEN  D  0
  THEN  Auto
  THEN  Try  ((OnVar  `fg'  (RWO  "rv-perm-point")\mcdot{}  THEN  Auto))
  THEN  Try  ((OnVar  `y'  (RWO  "rv-perm-point")\mcdot{}  THEN  Auto)))

---

Home Index