---

Step * 1 of Lemma rv-perp-same-norm


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))
BY
{ (Assert ||y|| = r1 BY
         (BLemma `rv-norm-eq-iff` THEN Auto THEN RWO "rnexp-one" 0 THEN Auto)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  ||y||  =  r1  BY
              (BLemma  `rv-norm-eq-iff`  THEN  Auto  THEN  RWO  "rnexp-one"  0  THEN  Auto))

---

Home Index