---

Step * 1 2 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)
⊢ u = 0 ∈ (ℕ3 ⟶ |r|)
BY
{ (FunExt THENA 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|
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|

---

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
\mvdash{}  u  =  0


By

---

Latex:
(FunExt  THENA  Auto)

---

Home Index