---

Step * of Lemma r2-det-syzygy

∀[p,q,r,u,v,w,x,y,z:ℝ^2].
  (((|pqw| * |rpv| * |qry| * |prx| * |quz|)
  + (|rpv| * |qru| * |rpz| * |qpy| * |qwx|)
  + (|qru| * |pqw| * |rpz| * |prx| * |qvy|)
  + (|qru| * |pqw| * |rpz| * |qpy| * |rvx|)
  + (|pqw| * |rpv| * |pqx| * |rqz| * |ruy|)
  + (|rpv| * |qru| * |pqx| * |qpy| * |rwz|)
  + (|rpv| * |qru| * |pqx| * |rqz| * |pwy|)
  + (|qru| * |pqw| * |qry| * |prx| * |pvz|)
  + (|pqw| * |rpv| * |qry| * |rqz| * |pux|))
  = r0)
BY
{ (Auto THEN Unfold `r2-det` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p,q,r,u,v,w,x,y,z:\mBbbR{}\^{}2].
    (((|pqw|  *  |rpv|  *  |qry|  *  |prx|  *  |quz|)
    +  (|rpv|  *  |qru|  *  |rpz|  *  |qpy|  *  |qwx|)
    +  (|qru|  *  |pqw|  *  |rpz|  *  |prx|  *  |qvy|)
    +  (|qru|  *  |pqw|  *  |rpz|  *  |qpy|  *  |rvx|)
    +  (|pqw|  *  |rpv|  *  |pqx|  *  |rqz|  *  |ruy|)
    +  (|rpv|  *  |qru|  *  |pqx|  *  |qpy|  *  |rwz|)
    +  (|rpv|  *  |qru|  *  |pqx|  *  |rqz|  *  |pwy|)
    +  (|qru|  *  |pqw|  *  |qry|  *  |prx|  *  |pvz|)
    +  (|pqw|  *  |rpv|  *  |qry|  *  |rqz|  *  |pux|))
    =  r0)


By

---

Latex:
(Auto  THEN  Unfold  `r2-det`  0  THEN  Auto)

---

Home Index