---

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

.....antecedent..... 
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)
⊢ (λi.[a; b; c][i]*matrix(u x)) = 0 ∈ Column(3;r)
BY
{ (Unfolds ``matrix-times zero-matrix`` 0 THEN EqCDA THEN Reduce 0 THEN RepUR ``matrix-ap`` 0) }

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|
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|

---

Latex:

---

Latex:
.....antecedent..... 
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)
\mvdash{}  (\mlambda{}i.[a;  b;  c][i]*matrix(u  x))  =  0


By

---

Latex:
(Unfolds  ``matrix-times  zero-matrix``  0  THEN  EqCDA  THEN  Reduce  0  THEN  RepUR  ``matrix-ap``  0)

---

Home Index