---

Step * 1 1 of Lemma rpolynomial-rmul


1. [n] : ℕ
2. [a] : ℕn + 1 ⟶ ℝ
3. [x] : ℝ
4. [b] : ℝ
5. (b * (Σi≤n. a_i * x^i)) = (Σi≤n. λi.(b * (a i))_i * x^i)
6. (b * (Σi≤n. a_i * x^i)) = ((Σi≤n. a_i * x^i) * b)
⊢ ((Σi≤n. a_i * x^i) * b) = (Σi≤n. λi.((a i) * b)_i * x^i)
BY
{ (Assert (Σi≤n. λi.(b * (a i))_i * x^i) = (Σi≤n. λi.((a i) * b)_i * x^i) BY
         (BLemma `rpolynomial_functionality` THEN Auto THEN D 0 THEN RepUR ``so_apply`` 0 THEN Auto)) }

1
1. [n] : ℕ
2. [a] : ℕn + 1 ⟶ ℝ
3. [x] : ℝ
4. [b] : ℝ
5. (b * (Σi≤n. a_i * x^i)) = (Σi≤n. λi.(b * (a i))_i * x^i)
6. (b * (Σi≤n. a_i * x^i)) = ((Σi≤n. a_i * x^i) * b)
7. (Σi≤n. λi.(b * (a i))_i * x^i) = (Σi≤n. λi.((a i) * b)_i * x^i)
⊢ ((Σi≤n. a_i * x^i) * b) = (Σi≤n. λi.((a i) * b)_i * x^i)

---

Latex:

---

Latex:

1.  [n]  :  \mBbbN{}
2.  [a]  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
3.  [x]  :  \mBbbR{}
4.  [b]  :  \mBbbR{}
5.  (b  *  (\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i))  =  (\mSigma{}i\mleq{}n.  \mlambda{}i.(b  *  (a  i))\_i  *  x\^{}i)
6.  (b  *  (\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i))  =  ((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  *  b)
\mvdash{}  ((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  *  b)  =  (\mSigma{}i\mleq{}n.  \mlambda{}i.((a  i)  *  b)\_i  *  x\^{}i)


By

---

Latex:
(Assert  (\mSigma{}i\mleq{}n.  \mlambda{}i.(b  *  (a  i))\_i  *  x\^{}i)  =  (\mSigma{}i\mleq{}n.  \mlambda{}i.((a  i)  *  b)\_i  *  x\^{}i)  BY
              (BLemma  `rpolynomial\_functionality`  THEN  Auto  THEN  D  0  THEN  RepUR  ``so\_apply``  0  THEN  Auto))

---

Home Index