---

Step * of Lemma r2-det-mul

∀[p,q,r:ℝ^2]. ∀[a:ℝ].  (|a*pqr| = ((a * |pqr|) + ((r1 - a) * (((q 0) * (r 1)) - (q 1) * (r 0)))))
BY
{ (Auto THEN RepUR ``r2-det real-vec-add real-vec-mul`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p,q,r:\mBbbR{}\^{}2].  \mforall{}[a:\mBbbR{}].    (|a*pqr|  =  ((a  *  |pqr|)  +  ((r1  -  a)  *  (((q  0)  *  (r  1))  -  (q  1)  *  (r  0)))))


By

---

Latex:
(Auto  THEN  RepUR  ``r2-det  real-vec-add  real-vec-mul``  0  THEN  Auto)

---

Home Index