---

Step * 1 of Lemma scalar-product-mul

.....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|
BY
{ (RepUR ``vector-mul`` 0 THEN RW RngNormC 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
4:n
1.  r  :  Rng
2.  n  :  \mBbbN{}
3.  a  :  \mBbbN{}n  {}\mrightarrow{}  |r|
4.  b  :  \mBbbN{}n  {}\mrightarrow{}  |r|
5.  c  :  |r|
6.  i  :  \mBbbN{}n
\mvdash{}  (((c*a)  i)  *  (b  i))  =  (c  *  ((a  i)  *  (b  i)))


By

---

Latex:
(RepUR  ``vector-mul``  0  THEN  RW  RngNormC  0  THEN  Auto)

---

Home Index