---

Step * 1 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|
⊢ (((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|
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{}  (((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


By

---

Latex:
(RW  CRngNormC  0  THEN  Auto)

---

Home Index