---

Step * 1 of Lemma rv-perp-1


1. rv : InnerProductSpace
2. x : Point(rv)
3. x # 0
4. y : Point(rv)
5. y # 0
6. x ⋅ y = r0
⊢ ∃y:Point(rv). ((y^2 = r1) ∧ (x ⋅ y = r0))
BY
{ (D 0 With ⌜rv-unit(rv;y)⌝  THEN EAuto 1) }

1
1. rv : InnerProductSpace
2. x : Point(rv)
3. x # 0
4. y : Point(rv)
5. y # 0
6. x ⋅ y = r0
7. rv-unit(rv;y)^2 = r1
⊢ x ⋅ rv-unit(rv;y) = r0

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  x  :  Point(rv)
3.  x  \#  0
4.  y  :  Point(rv)
5.  y  \#  0
6.  x  \mcdot{}  y  =  r0
\mvdash{}  \mexists{}y:Point(rv).  ((y\^{}2  =  r1)  \mwedge{}  (x  \mcdot{}  y  =  r0))


By

---

Latex:
(D  0  With  \mkleeneopen{}rv-unit(rv;y)\mkleeneclose{}    THEN  EAuto  1)

---

Home Index