---

Step * of Lemma scalar-product-add-left

∀[r:Rng]. ∀[n:ℕ]. ∀[a,b,c:ℕn ⟶ |r|].  (((a + b) . c) = ((a . c) +r (b . c)) ∈ |r|)
BY
{ (Auto
   THEN RepUR ``scalar-product vector-add`` 0
   THEN (RWO "rng_sum_plus<" 0 THENA Auto)
   THEN EqCDA
   THEN RW RngNormC 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[n:\mBbbN{}].  \mforall{}[a,b,c:\mBbbN{}n  {}\mrightarrow{}  |r|].    (((a  +  b)  .  c)  =  ((a  .  c)  +r  (b  .  c)))


By

---

Latex:
(Auto
  THEN  RepUR  ``scalar-product  vector-add``  0
  THEN  (RWO  "rng\_sum\_plus<"  0  THENA  Auto)
  THEN  EqCDA
  THEN  RW  RngNormC  0
  THEN  Auto)

---

Home Index