---

Step * 2 of Lemma rv-ip-rneq


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. a2 ⋅ b2 ≠ a2 ⋅ b1
⊢ b1 # b2
BY
{ (InstLemma `rv-ip-rneq-0` [⌜rv⌝;⌜a2⌝;⌜b2 - b1⌝]⋅ THEN EAuto 2) }

1
.....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. a2 ⋅ b2 ≠ a2 ⋅ b1
⊢ a2 ⋅ b2 - b1 ≠ r0

---

Latex:

---

Latex:

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.  a2  \mcdot{}  b2  \mneq{}  a2  \mcdot{}  b1
\mvdash{}  b1  \#  b2


By

---

Latex:
(InstLemma  `rv-ip-rneq-0`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}b2  -  b1\mkleeneclose{}]\mcdot{}  THEN  EAuto  2)

---

Home Index