---

Step * of Lemma r2-dot-product

∀[a,b:ℝ^2].  (a⋅b = (((a 0) * (b 0)) + ((a 1) * (b 1))))
BY
{ (Auto
   THEN RepUR ``dot-product`` 0
   THEN (RWO "rsum-split-first" 0 THENA Auto)
   THEN Reduce 0
   THEN RWO "rsum-single" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbR{}\^{}2].    (a\mcdot{}b  =  (((a  0)  *  (b  0))  +  ((a  1)  *  (b  1))))


By

---

Latex:
(Auto
  THEN  RepUR  ``dot-product``  0
  THEN  (RWO  "rsum-split-first"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RWO  "rsum-single"  0
  THEN  Auto)

---

Home Index