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