---

Step * of Lemma trans-kernel-is-kernel-fun

∀rv:InnerProductSpace. ∀e:Point. ∀T:ℝ ⟶ Point ⟶ Point.
  ((e^2 = r1) ⇒ translation-group-fun(rv;e;T) ⇒ trans-kernel-fun(rv;e;λh,t. ρ(h;t)))
BY
{ (Auto
   THEN D 0
   THEN Reduce 0
   THEN Auto
   THEN Try ((Assert h ⋅ e = r0 BY (DVar `h' THEN Unhide THEN Auto)))
   THEN RepUR ``trans-kernel`` 0) }

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. t1 : ℝ
9. t2 : ℝ
10. ρ(h1;t1) ≠ ρ(h2;t2)
⊢ h1 # h2 ∨ t1 ≠ t2

2
1. rv : InnerProductSpace
2. e : Point
3. T : ℝ ⟶ Point ⟶ Point
4. e^2 = r1
5. translation-group-fun(rv;e;T)
6. h : {h:Point| h ⋅ e = r0} 
7. h ⋅ e = r0
⊢ T_r0(h) ⋅ e = r0

3
1. rv : InnerProductSpace
2. e : Point
3. T : ℝ ⟶ Point ⟶ Point
4. e^2 = r1
5. translation-group-fun(rv;e;T)
6. ∀h:{h:Point| h ⋅ e = r0} . (ρ(h;r0) = r0)
7. h : {h:Point| h ⋅ e = r0} 
8. t1 : ℝ
9. t2 : ℝ
10. t1 < t2
11. h ⋅ e = r0
⊢ T_t1(h) ⋅ e < T_t2(h) ⋅ e

4
1. rv : InnerProductSpace
2. e : Point
3. T : ℝ ⟶ Point ⟶ Point
4. e^2 = r1
5. translation-group-fun(rv;e;T)
6. ∀h:{h:Point| h ⋅ e = r0} . (ρ(h;r0) = r0)
7. ∀h:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ.  ((t1 < t2) ⇒ (ρ(h;t1) < ρ(h;t2)))
8. h : {h:Point| h ⋅ e = r0} 
9. r : ℝ
10. h ⋅ e = r0
⊢ ∃t:ℝ. (T_t(h) ⋅ e = r)

---

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{}  trans-kernel-fun(rv;e;\mlambda{}h,t.  \mrho{}(h;t)))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((Assert  h  \mcdot{}  e  =  r0  BY  (DVar  `h'  THEN  Unhide  THEN  Auto)))
  THEN  RepUR  ``trans-kernel``  0)

---

Home Index