---

Step * of Lemma trans-apply-0

∀rv:InnerProductSpace. ∀T:ℝ ⟶ Point ⟶ Point.  ∀x:Point. T_r0(x) ≡ x supposing ∃e:Point. translation-group-fun(rv;e;T)
BY
{ ((Auto THEN ExRepD) THEN (Assert translation-group-fun(rv;e;T) BY Auto) THEN D -3 THEN ExRepD) }

1
1. rv : InnerProductSpace
2. T : ℝ ⟶ Point ⟶ Point
3. e : 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:ℝ. (y ≠ t ⇒ T y x # x + r*e)))
7. ∀x:Point. ∀t:{t:ℝ| r0 ≤ t} .  ∃r:{t:ℝ| r0 ≤ t} . T t x ≡ x + r*e
8. x : Point
9. translation-group-fun(rv;e;T)
⊢ T_r0(x) ≡ x

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}T:\mBbbR{}  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point.
    \mforall{}x:Point.  T\_r0(x)  \mequiv{}  x  supposing  \mexists{}e:Point.  translation-group-fun(rv;e;T)


By

---

Latex:
((Auto  THEN  ExRepD)  THEN  (Assert  translation-group-fun(rv;e;T)  BY  Auto)  THEN  D  -3  THEN  ExRepD)

---

Home Index