---

Step * of Lemma trans-kernel_functionality

∀rv:InnerProductSpace. ∀e:Point. ∀T:ℝ ⟶ Point ⟶ Point.
  ((e^2 = r1)
  ⇒ translation-group-fun(rv;e;T)
  ⇒ (∀h1,h2:{h:Point| h ⋅ e = r0} . ∀t,s:ℝ.  (ρ(h1;t) = ρ(h2;s)) supposing ((t = s) and h1 ≡ h2)))
BY
{ (Auto THEN (FLemma `trans-kernel-is-kernel-fun` [5] THENA Auto) THEN D -1 THEN Thin (-1) THEN Reduce -1) }

1
1. rv : InnerProductSpace
2. e : Point
3. T : ℝ ⟶ Point ⟶ Point
4. e^2 = r1
5. translation-group-fun(rv;e;T)
6. h1 : {h:Point| h ⋅ e = r0} 
7. h2 : {h:Point| h ⋅ e = r0} 
8. t : ℝ
9. s : ℝ
10. h1 ≡ h2
11. t = s
12. ∀h1,h2:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ.  (ρ(h1;t1) ≠ ρ(h2;t2) ⇒ (h1 # h2 ∨ t1 ≠ t2))
⊢ ρ(h1;t) = ρ(h2;s)

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}e:Point.  \mforall{}T:\mBbbR{}  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point.
    ((e\^{}2  =  r1)
    {}\mRightarrow{}  translation-group-fun(rv;e;T)
    {}\mRightarrow{}  (\mforall{}h1,h2:\{h:Point|  h  \mcdot{}  e  =  r0\}  .  \mforall{}t,s:\mBbbR{}.    (\mrho{}(h1;t)  =  \mrho{}(h2;s))  supposing  ((t  =  s)  and  h1  \mequiv{}  h2)))


By

---

Latex:
(Auto
  THEN  (FLemma  `trans-kernel-is-kernel-fun`  [5]  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  Reduce  -1)

---

Home Index