---

Step * of Lemma rv-decomp_wf

∀[rv:InnerProductSpace]. ∀[e,x:Point].  rv-decomp(rv;x;e) ∈ {p:Point × ℝ| x ≡ fst(p) + snd(p)*e ∧ (fst(p) ⋅ e = r0)}  su\000Cpposing e^2 = r1
BY
{ (Auto
   THEN Unfold `rv-decomp` 0
   THEN MemTypeCD
   THEN Auto
   THEN Reduce 0
   THEN RepeatFor 3 ((RWO "rv-ip-sub rv-ip-mul 4 rv-sub-add" 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[e,x:Point].
    rv-decomp(rv;x;e)  \mmember{}  \{p:Point  \mtimes{}  \mBbbR{}|  x  \mequiv{}  fst(p)  +  snd(p)*e  \mwedge{}  (fst(p)  \mcdot{}  e  =  r0)\}    supposing  e\^{}2  =  r1


By

---

Latex:
(Auto
  THEN  Unfold  `rv-decomp`  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  Reduce  0
  THEN  RepeatFor  3  ((RWO  "rv-ip-sub  rv-ip-mul  4  rv-sub-add"  0  THEN  Auto)))

---

Home Index