---

Step * of Lemma trans-from-kernel_wf

∀[rv:InnerProductSpace]. ∀[e:{e:Point| e^2 = r1} ]. ∀[f,g:{h:Point| h ⋅ e = r0}  ⟶ ℝ ⟶ ℝ]. ∀[t:ℝ]. ∀[x:Point].
  (trans-from-kernel(rv;e;f;g;t;x) ∈ Point)
BY
{ (ProveWfLemma THEN MemTypeCD THEN Auto THEN (RWW "rv-ip-sub rv-ip-mul 3" 0 THENA Auto) THEN nRNorm 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[e:\{e:Point|  e\^{}2  =  r1\}  ].  \mforall{}[f,g:\{h:Point|  h  \mcdot{}  e  =  r0\}    {}\mrightarrow{}  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[t:\mBbbR{}].
\mforall{}[x:Point].
    (trans-from-kernel(rv;e;f;g;t;x)  \mmember{}  Point)


By

---

Latex:
(ProveWfLemma
  THEN  MemTypeCD
  THEN  Auto
  THEN  (RWW  "rv-ip-sub  rv-ip-mul  3"  0  THENA  Auto)
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index