---

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


By

---

Latex:
(RW  CRngNormC  0  THEN  Auto)

---

Home Index