---

Step * of Lemma scalar-triple-product-non-zero

∀[r:IntegDom{i}]. ∀[a,b,c:ℕ3 ⟶ |r|].
  ∀[u:ℕ3 ⟶ |r|]. (((a . u) = 0 ∈ |r|) ⇒ ((b . u) = 0 ∈ |r|) ⇒ ((c . u) = 0 ∈ |r|) ⇒ (u = 0 ∈ (ℕ3 ⟶ |r|))) 
  supposing ¬(|a,b,c| = 0 ∈ |r|)
BY
{ (InstLemma `scalar-triple-product-as-det` [] THEN RepeatFor 4 (ParallelLast') THEN Auto) }

1
1. r : IntegDom{i}
2. a : ℕ3 ⟶ |r|
3. b : ℕ3 ⟶ |r|
4. c : ℕ3 ⟶ |r|
5. |a,b,c| = |λi.[a; b; c][i]| ∈ |r|
6. ¬(|a,b,c| = 0 ∈ |r|)
7. u : ℕ3 ⟶ |r|
8. (a . u) = 0 ∈ |r|
9. (b . u) = 0 ∈ |r|
10. (c . u) = 0 ∈ |r|
⊢ u = 0 ∈ (ℕ3 ⟶ |r|)

---

Latex:

---

Latex:
\mforall{}[r:IntegDom\{i\}].  \mforall{}[a,b,c:\mBbbN{}3  {}\mrightarrow{}  |r|].
    \mforall{}[u:\mBbbN{}3  {}\mrightarrow{}  |r|].  (((a  .  u)  =  0)  {}\mRightarrow{}  ((b  .  u)  =  0)  {}\mRightarrow{}  ((c  .  u)  =  0)  {}\mRightarrow{}  (u  =  0)) 
    supposing  \mneg{}(|a,b,c|  =  0)


By

---

Latex:
(InstLemma  `scalar-triple-product-as-det`  []  THEN  RepeatFor  4  (ParallelLast')  THEN  Auto)

---

Home Index