---

Step * of Lemma scalar-product-mul

∀[r:Rng]. ∀[n:ℕ]. ∀[a,b:ℕn ⟶ |r|]. ∀[c:|r|].  (((c*a) . b) = (c * (a . b)) ∈ |r|)
BY
{ ((Auto THEN Unfold `scalar-product` 0) THEN (RWO "rng_times_sum_l" 0 THENA Auto) THEN EqCDA) }

1
.....subterm..... T:t
4:n
1. r : Rng
2. n : ℕ
3. a : ℕn ⟶ |r|
4. b : ℕn ⟶ |r|
5. c : |r|
6. i : ℕn
⊢ (((c*a) i) * (b i)) = (c * ((a i) * (b i))) ∈ |r|

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  Unfold  `scalar-product`  0)  THEN  (RWO  "rng\_times\_sum\_l"  0  THENA  Auto)  THEN  EqCDA)

---

Home Index