---

Step * 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|
⊢ u = 0 ∈ (ℕ3 ⟶ |r|)
BY
{ ((Assert λi.[a; b; c][i] ∈ Matrix(3;3;r) BY
          (Unfold `matrix` 0 THEN Auto))
   THEN InstLemma `null-space-unique` [⌜r⌝;⌜3⌝;⌜λi.[a; b; c][i]⌝;⌜matrix(u x)⌝]⋅
   THEN Auto) }

1
.....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)

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

---

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


By

---

Latex:
((Assert  \mlambda{}i.[a;  b;  c][i]  \mmember{}  Matrix(3;3;r)  BY
                (Unfold  `matrix`  0  THEN  Auto))
  THEN  InstLemma  `null-space-unique`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}3\mkleeneclose{};\mkleeneopen{}\mlambda{}i.[a;  b;  c][i]\mkleeneclose{};\mkleeneopen{}matrix(u  x)\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index