---

Step * of Lemma test-ring-eq

∀[r:CRng]
  ∀v,v1,v2,v3,v4,v5,v6,v7,v8,v9:|r|.
    ((((((v6 * v3) +r ((v2 * v5) +r (v4 * v7))) +r (-r ((v7 * v2) +r ((v3 * v4) +r (v5 * v6))))) 
       * 
       (((v6 * v9) +r ((v8 * v1) +r (v * v7))) +r (-r ((v7 * v8) +r ((v9 * v) +r (v1 * v6)))))) 
      +r 
      (((((v * v7) +r ((v6 * v5) +r (v4 * v1))) +r (-r ((v1 * v6) +r ((v7 * v4) +r (v5 * v))))) 
        * 
        (((v6 * v9) +r ((v8 * v3) +r (v2 * v7))) +r (-r ((v7 * v8) +r ((v9 * v2) +r (v3 * v6)))))) 
       +r 
       ((((v * v3) +r ((v2 * v7) +r (v6 * v1))) +r (-r ((v1 * v2) +r ((v3 * v6) +r (v7 * v))))) 
        * 
        (((v6 * v9) +r ((v8 * v5) +r (v4 * v7))) +r (-r ((v7 * v8) +r ((v9 * v4) +r (v5 * v6))))))))
    = 0
    ∈ |r|)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[r:CRng]
    \mforall{}v,v1,v2,v3,v4,v5,v6,v7,v8,v9:|r|.
        ((((((v6  *  v3)  +r  ((v2  *  v5)  +r  (v4  *  v7)))  +r  (-r  ((v7  *  v2)  +r  ((v3  *  v4)  +r  (v5  *  v6))))) 
              * 
              (((v6  *  v9)  +r  ((v8  *  v1)  +r  (v  *  v7)))  +r  (-r  ((v7  *  v8)  +r  ((v9  *  v)  +r  (v1  *  v6)))))) 
            +r 
            (((((v  *  v7)  +r  ((v6  *  v5)  +r  (v4  *  v1)))  +r  (-r  ((v1  *  v6)  +r  ((v7  *  v4)  +r  (v5  *  v))))) 
                * 
                (((v6  *  v9)  +r  ((v8  *  v3)  +r  (v2  *  v7)))  +r  (-r  ((v7  *  v8)  +r  ((v9  *  v2)  +r  (v3  *  v6)))))) 
              +r 
              ((((v  *  v3)  +r  ((v2  *  v7)  +r  (v6  *  v1)))  +r  (-r  ((v1  *  v2)  +r  ((v3  *  v6)  +r  (v7  *  v))))) 
                * 
                (((v6  *  v9)  +r  ((v8  *  v5)  +r  (v4  *  v7)))  +r  (-r  ((v7  *  v8)  +r  ((v9  *  v4)  +r  (v5  *  v6))))))))
        =  0)


By

---

Latex:
Auto

---

Home Index