---

Step * of Lemma rv-ip-rneq

No Annotations
∀rv:InnerProductSpace. ∀a1,b1,a2,b2:Point(rv).  (a1 ⋅ b1 ≠ a2 ⋅ b2 ⇒ (a1 # a2 ∨ b1 # b2))
BY
{ (Auto THEN (InstLemma `rneq-cases` [⌜a1 ⋅ b1⌝;⌜a2 ⋅ b2⌝;⌜a2 ⋅ b1⌝]⋅ THENA Auto) THEN ParallelLast) }

1
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

2
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

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}a1,b1,a2,b2:Point(rv).    (a1  \mcdot{}  b1  \mneq{}  a2  \mcdot{}  b2  {}\mRightarrow{}  (a1  \#  a2  \mvee{}  b1  \#  b2))


By

---

Latex:
(Auto  THEN  (InstLemma  `rneq-cases`  [\mkleeneopen{}a1  \mcdot{}  b1\mkleeneclose{};\mkleeneopen{}a2  \mcdot{}  b2\mkleeneclose{};\mkleeneopen{}a2  \mcdot{}  b1\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ParallelLast)

---

Home Index