---

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

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. a1 ⋅ b1 ≠ a2 ⋅ b1
⊢ a1 - a2 ⋅ 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.  a1  \mcdot{}  b1  \mneq{}  a2  \mcdot{}  b1
\mvdash{}  a1  \#  a2


By

---

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

---

Home Index