---

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


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
BY
{ (RWW "trans-apply-0 -1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  e  :  Point
3.  T  :  \mBbbR{}  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point
4.  e\^{}2  =  r1
5.  translation-group-fun(rv;e;T)
6.  h  :  \{h:Point|  h  \mcdot{}  e  =  r0\} 
7.  h  \mcdot{}  e  =  r0
\mvdash{}  T\_r0(h)  \mcdot{}  e  =  r0


By

---

Latex:
(RWW  "trans-apply-0  -1"  0  THEN  Auto)

---

Home Index