---

Step * of Lemma trans-apply-add

∀rv:InnerProductSpace. ∀T:ℝ ⟶ Point ⟶ Point. ∀t,s:ℝ.
  ∀x:Point. T_t + s(x) ≡ T_t(T_s(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
   THEN All  (Fold  `trans-apply`)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}T:\mBbbR{}  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point.  \mforall{}t,s:\mBbbR{}.
    \mforall{}x:Point.  T\_t  +  s(x)  \mequiv{}  T\_t(T\_s(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
  THEN  All    (Fold    `trans-apply`)
  THEN  Auto)

---

Home Index