---

Step * 1 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
7. ||y|| = r1
⊢ ∃y:Point. ((||y|| = ||x||) ∧ (x ⋅ y = r0))
BY
{ (D 0 With ⌜||x||*y⌝  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
⊢ ||||x||*y|| = ||x||

2
1. rv : InnerProductSpace
2. x : Point
3. x # 0
4. y : Point
5. y^2 = r1
6. x ⋅ y = r0
7. ||y|| = r1
8. ||||x||*y|| = ||x||
⊢ 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
7.  ||y||  =  r1
\mvdash{}  \mexists{}y:Point.  ((||y||  =  ||x||)  \mwedge{}  (x  \mcdot{}  y  =  r0))


By

---

Latex:
(D  0  With  \mkleeneopen{}||x||*y\mkleeneclose{}    THEN  Auto)

---

Home Index