---

Step * of Lemma another-r2-det-identity

∀[p,q,r,t,s:ℝ^2].  (((|tqr| * |tsp|) + (|ptr| * |tsq|) + (|pqt| * |tsr|)) = r0)
BY
{ (Auto THEN Unfold `r2-det` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p,q,r,t,s:\mBbbR{}\^{}2].    (((|tqr|  *  |tsp|)  +  (|ptr|  *  |tsq|)  +  (|pqt|  *  |tsr|))  =  r0)


By

---

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

---

Home Index