---

Step * of Lemma trans-kernel-equation

∀[rv:InnerProductSpace]. ∀[e:{e:Point| e^2 = r1} ]. ∀[T:ℝ ⟶ Point ⟶ Point].
  ∀[t:ℝ]. ∀[h:{h:Point| h ⋅ e = r0} ].  T_t(h) ≡ h + ρ(h;t)*e supposing translation-group-fun(rv;e;T)
BY
{ (Auto THEN DSetVars THEN Unhide THEN Auto THEN D -4 THEN Auto THEN All (Fold `trans-apply`)) }

1
1. rv : InnerProductSpace
2. e : Point
3. e^2 = r1
4. T : ℝ ⟶ Point ⟶ Point
5. ∀s,t:ℝ. ∀x,y:Point.  (T_s(x) # T_t(y) ⇒ (x # y ∨ s ≠ t))
6. ∀t,s:ℝ. ∀x:Point.  T_t + s(x) ≡ T_t(T_s(x))
7. ∀x:Point. ∀r:ℝ.  ∃t:ℝ. (T_t(x) ≡ x + r*e ∧ (∀y:ℝ. (y ≠ t ⇒ T_y(x) # x + r*e)))
8. ∀x:Point. ∀t:{t:ℝ| r0 ≤ t} .  ∃r:{t:ℝ| r0 ≤ t} . T_t(x) ≡ x + r*e
9. t : ℝ
10. h : Point
11. h ⋅ e = r0
⊢ T_t(h) ≡ h + ρ(h;t)*e

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[e:\{e:Point|  e\^{}2  =  r1\}  ].  \mforall{}[T:\mBbbR{}  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point].
    \mforall{}[t:\mBbbR{}].  \mforall{}[h:\{h:Point|  h  \mcdot{}  e  =  r0\}  ].    T\_t(h)  \mequiv{}  h  +  \mrho{}(h;t)*e  supposing  translation-group-fun(rv;e;T\000C)


By

---

Latex:
(Auto  THEN  DSetVars  THEN  Unhide  THEN  Auto  THEN  D  -4  THEN  Auto  THEN  All  (Fold  `trans-apply`))

---

Home Index