---

Step * of Lemma rv-perp-1

No Annotations
∀rv:InnerProductSpace. ∀x:Point(rv).  (x # 0 ⇒ (∃y:Point(rv). ((y^2 = r1) ∧ (x ⋅ y = r0))))
BY
{ ((D 0 THENA Auto)
   THEN (Assert ∀x:Point(rv). (x # 0 ⇒ (∃y:Point(rv). (y # 0 ∧ (x ⋅ y = r0)))) BY
               (UseWitness ⌜rv."perp"⌝⋅ THEN (D 1 THENA Auto) THEN Unfold `rv-ip` 0 THEN Trivial))
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN ExRepD) }

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))

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}x:Point(rv).    (x  \#  0  {}\mRightarrow{}  (\mexists{}y:Point(rv).  ((y\^{}2  =  r1)  \mwedge{}  (x  \mcdot{}  y  =  r0))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  \mforall{}x:Point(rv).  (x  \#  0  {}\mRightarrow{}  (\mexists{}y:Point(rv).  (y  \#  0  \mwedge{}  (x  \mcdot{}  y  =  r0))))  BY
                          (UseWitness  \mkleeneopen{}rv."perp"\mkleeneclose{}\mcdot{}  THEN  (D  1  THENA  Auto)  THEN  Unfold  `rv-ip`  0  THEN  Trivial))
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  ExRepD)

---

Home Index