---

Step * 2 of Lemma Jacobi-identity


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|
BY
{ (RW CRngNormC 0 THEN Auto) }

---

Latex:

---

Latex:

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|
\mvdash{}  (((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


By

---

Latex:
(RW  CRngNormC  0  THEN  Auto)

---

Home Index