---

Step * of Lemma scalar-product-3

∀[r,a,b:Top].  ((a . b) ~ ((0 +r ((a 0) * (b 0))) +r ((a 1) * (b 1))) +r ((a 2) * (b 2)))
BY
{ ((Auto THEN RepUR ``scalar-product cross-product rng_sum mon_itop`` 0)
   THEN RepeatFor 4 ((RecUnfold `itop` 0 THEN Reduce 0))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r,a,b:Top].    ((a  .  b)  \msim{}  ((0  +r  ((a  0)  *  (b  0)))  +r  ((a  1)  *  (b  1)))  +r  ((a  2)  *  (b  2)))


By

---

Latex:
((Auto  THEN  RepUR  ``scalar-product  cross-product  rng\_sum  mon\_itop``  0)
  THEN  RepeatFor  4  ((RecUnfold  `itop`  0  THEN  Reduce  0))
  THEN  Auto)

---

Home Index