---

Step * 1 2 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. matrix(u x) = 0 ∈ Column(3;r)
13. x : ℕ3
⊢ (u x) = (0 x) ∈ |r|
BY
{ ((ApFunToHypEquands `M' ⌜M[x,0]⌝ ⌜|r|⌝ (-2)⋅ THENA Auto) THEN RepUR ``zero-matrix`` -1) }

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. matrix(u x) = 0 ∈ Column(3;r)
13. x : ℕ3
14. (u x) = 0 ∈ |r|
⊢ (u x) = (0 x) ∈ |r|

---

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.  matrix(u  x)  =  0
13.  x  :  \mBbbN{}3
\mvdash{}  (u  x)  =  (0  x)


By

---

Latex:
((ApFunToHypEquands  `M'  \mkleeneopen{}M[x,0]\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)  THEN  RepUR  ``zero-matrix``  -1)

---

Home Index