---

Step * of Lemma Jacobi-identity

∀[r:CRng]. ∀[a,b,c:ℕ3 ⟶ |r|].  (((a x (b x c)) + ((b x (c x a)) + (c x (a x b)))) = 0 ∈ (ℕ3 ⟶ |r|))
BY
{ (Intros
   THEN (FunExt THENW Auto)
   THEN IntSegCases (-1)
   THEN RepUR ``cross-product vector-add zero-vector`` 0
   THEN GenConclTerms Auto [⌜a 0⌝;⌜a 1⌝;⌜a 2⌝;⌜b 0⌝;⌜b 1⌝;⌜b 2⌝;⌜c 0⌝;⌜c 1⌝;⌜c 2⌝]⋅
   THEN All  Thin) }

1
1. r : CRng
2. v : |r|
3. v1 : |r|
4. v2 : |r|
5. v3 : |r|
6. v4 : |r|
7. v5 : |r|
8. v6 : |r|
9. v7 : |r|
10. v8 : |r|
⊢ (((v1 * ((v3 * v7) +r (-r (v4 * v6)))) +r (-r (v2 * ((v5 * v6) +r (-r (v3 * v8)))))) 
   +r 
   (((v4 * ((v6 * v1) +r (-r (v7 * v)))) +r (-r (v5 * ((v8 * v) +r (-r (v6 * v2)))))) 
    +r 
    ((v7 * ((v * v4) +r (-r (v1 * v3)))) +r (-r (v8 * ((v2 * v3) +r (-r (v * v5))))))))
= 0
∈ |r|

2
1. r : CRng
2. v : |r|
3. v1 : |r|
4. v2 : |r|
5. v3 : |r|
6. v4 : |r|
7. v5 : |r|
8. v6 : |r|
9. v7 : |r|
10. v8 : |r|
⊢ (((v2 * ((v4 * v8) +r (-r (v5 * v7)))) +r (-r (v * ((v3 * v7) +r (-r (v4 * v6)))))) 
   +r 
   (((v5 * ((v7 * v2) +r (-r (v8 * v1)))) +r (-r (v3 * ((v6 * v1) +r (-r (v7 * v)))))) 
    +r 
    ((v8 * ((v1 * v5) +r (-r (v2 * v4)))) +r (-r (v6 * ((v * v4) +r (-r (v1 * v3))))))))
= 0
∈ |r|

3
1. r : CRng
2. v : |r|
3. v1 : |r|
4. v2 : |r|
5. v3 : |r|
6. v4 : |r|
7. v5 : |r|
8. v6 : |r|
9. v7 : |r|
10. v8 : |r|
⊢ (((v * ((v5 * v6) +r (-r (v3 * v8)))) +r (-r (v1 * ((v4 * v8) +r (-r (v5 * v7)))))) 
   +r 
   (((v3 * ((v8 * v) +r (-r (v6 * v2)))) +r (-r (v4 * ((v7 * v2) +r (-r (v8 * v1)))))) 
    +r 
    ((v6 * ((v2 * v3) +r (-r (v * v5)))) +r (-r (v7 * ((v1 * v5) +r (-r (v2 * v4))))))))
= 0
∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[a,b,c:\mBbbN{}3  {}\mrightarrow{}  |r|].    (((a  x  (b  x  c))  +  ((b  x  (c  x  a))  +  (c  x  (a  x  b))))  =  0)


By

---

Latex:
(Intros
  THEN  (FunExt  THENW  Auto)
  THEN  IntSegCases  (-1)
  THEN  RepUR  ``cross-product  vector-add  zero-vector``  0
  THEN  GenConclTerms  Auto  [\mkleeneopen{}a  0\mkleeneclose{};\mkleeneopen{}a  1\mkleeneclose{};\mkleeneopen{}a  2\mkleeneclose{};\mkleeneopen{}b  0\mkleeneclose{};\mkleeneopen{}b  1\mkleeneclose{};\mkleeneopen{}b  2\mkleeneclose{};\mkleeneopen{}c  0\mkleeneclose{};\mkleeneopen{}c  1\mkleeneclose{};\mkleeneopen{}c  2\mkleeneclose{}]\mcdot{}
  THEN  All    Thin)

---

Home Index