---

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


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|
11. λi.[a; b; c][i] ∈ Matrix(3;3;r)
12. x : ℕ3
13. y : ℕ1
⊢ (Σ(r) 0 ≤ i < 3. ([a; b; c][x] i) * (u i)) = 0 ∈ |r|
BY
{ ((IntSegCases (-2) THEN Reduce 0) THEN Fold `scalar-product` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}
2.  a  :  \mBbbN{}3  {}\mrightarrow{}  |r|
3.  b  :  \mBbbN{}3  {}\mrightarrow{}  |r|
4.  c  :  \mBbbN{}3  {}\mrightarrow{}  |r|
5.  |a,b,c|  =  |\mlambda{}i.[a;  b;  c][i]|
6.  \mneg{}(|a,b,c|  =  0)
7.  u  :  \mBbbN{}3  {}\mrightarrow{}  |r|
8.  (a  .  u)  =  0
9.  (b  .  u)  =  0
10.  (c  .  u)  =  0
11.  \mlambda{}i.[a;  b;  c][i]  \mmember{}  Matrix(3;3;r)
12.  x  :  \mBbbN{}3
13.  y  :  \mBbbN{}1
\mvdash{}  (\mSigma{}(r)  0  \mleq{}  i  <  3.  ([a;  b;  c][x]  i)  *  (u  i))  =  0


By

---

Latex:
((IntSegCases  (-2)  THEN  Reduce  0)  THEN  Fold  `scalar-product`  0  THEN  Auto)

---

Home Index