---

Step * of Lemma rv-perp-same-norm

∀rv:InnerProductSpace. ∀x:Point.  (x # 0 ⇒ (∃y:Point. ((||y|| = ||x||) ∧ (x ⋅ y = r0))))
BY
{ (InstLemma `rv-perp-1` [] THEN RepeatFor 3 (ParallelLast') THEN Auto THEN ExRepD) }

1
1. rv : InnerProductSpace
2. x : Point
3. x # 0
4. y : Point
5. y^2 = r1
6. x ⋅ y = r0
⊢ ∃y:Point. ((||y|| = ||x||) ∧ (x ⋅ y = r0))

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}x:Point.    (x  \#  0  {}\mRightarrow{}  (\mexists{}y:Point.  ((||y||  =  ||x||)  \mwedge{}  (x  \mcdot{}  y  =  r0))))


By

---

Latex:
(InstLemma  `rv-perp-1`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  Auto  THEN  ExRepD)

---

Home Index