---

Step * 1 1 of Lemma rv-ip-rneq

.....antecedent..... 
1. rv : InnerProductSpace
2. a1 : Point(rv)
3. b1 : Point(rv)
4. a2 : Point(rv)
5. b2 : Point(rv)
6. a1 ⋅ b1 ≠ a2 ⋅ b2
7. a1 ⋅ b1 ≠ a2 ⋅ b1
⊢ a1 - a2 ⋅ b1 ≠ r0
BY
{ (RWO "rv-ip-sub" 0 THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  rv  :  InnerProductSpace
2.  a1  :  Point(rv)
3.  b1  :  Point(rv)
4.  a2  :  Point(rv)
5.  b2  :  Point(rv)
6.  a1  \mcdot{}  b1  \mneq{}  a2  \mcdot{}  b2
7.  a1  \mcdot{}  b1  \mneq{}  a2  \mcdot{}  b1
\mvdash{}  a1  -  a2  \mcdot{}  b1  \mneq{}  r0


By

---

Latex:
(RWO  "rv-ip-sub"  0  THEN  Auto)

---

Home Index