---

Step * of Lemma scalar-product-add-right

∀[r:Rng]. ∀[n:ℕ]. ∀[a,b,c:ℕn ⟶ |r|].  ((c . (a + b)) = ((c . a) +r (c . b)) ∈ |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|].    ((c  .  (a  +  b))  =  ((c  .  a)  +r  (c  .  b)))


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