---

Step * 1 of Lemma ip-non-trivial


1. rv : InnerProductSpace
2. x : {x:Point| r0 < ||x||} 
⊢ ∃b:{Point| x # b}
BY
{ ((InstLemma `rv-perp-1` [⌜rv⌝;⌜x⌝]⋅ THENA EAuto 1) THEN ExRepD) }

1
1. rv : InnerProductSpace
2. x : {x:Point| r0 < ||x||} 
3. y : Point
4. y^2 = r1
5. x ⋅ y = r0
⊢ ∃b:{Point| x # b}

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  x  :  \{x:Point|  r0  <  ||x||\} 
\mvdash{}  \mexists{}b:\{Point|  x  \#  b\}


By

---

Latex:
((InstLemma  `rv-perp-1`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)  THEN  ExRepD)

---

Home Index