# Metamath Proof Explorer

## Theorem ply1mulr

Description: Value of multiplication in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses ply1plusg.y ${⊢}{Y}={\mathrm{Poly}}_{1}\left({R}\right)$
ply1plusg.s ${⊢}{S}={1}_{𝑜}\mathrm{mPoly}{R}$
ply1mulr.n
Assertion ply1mulr

### Proof

Step Hyp Ref Expression
1 ply1plusg.y ${⊢}{Y}={\mathrm{Poly}}_{1}\left({R}\right)$
2 ply1plusg.s ${⊢}{S}={1}_{𝑜}\mathrm{mPoly}{R}$
3 ply1mulr.n
4 eqid ${⊢}{1}_{𝑜}\mathrm{mPwSer}{R}={1}_{𝑜}\mathrm{mPwSer}{R}$
5 eqid ${⊢}{\cdot }_{{S}}={\cdot }_{{S}}$
6 2 4 5 mplmulr ${⊢}{\cdot }_{{S}}={\cdot }_{\left({1}_{𝑜}\mathrm{mPwSer}{R}\right)}$
7 eqid ${⊢}{\mathrm{PwSer}}_{1}\left({R}\right)={\mathrm{PwSer}}_{1}\left({R}\right)$
8 eqid ${⊢}{\cdot }_{{\mathrm{PwSer}}_{1}\left({R}\right)}={\cdot }_{{\mathrm{PwSer}}_{1}\left({R}\right)}$
9 7 4 8 psr1mulr ${⊢}{\cdot }_{{\mathrm{PwSer}}_{1}\left({R}\right)}={\cdot }_{\left({1}_{𝑜}\mathrm{mPwSer}{R}\right)}$
10 fvex ${⊢}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}\in \mathrm{V}$
11 1 7 ply1val ${⊢}{Y}={\mathrm{PwSer}}_{1}\left({R}\right){↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
12 11 8 ressmulr ${⊢}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}\in \mathrm{V}\to {\cdot }_{{\mathrm{PwSer}}_{1}\left({R}\right)}={\cdot }_{{Y}}$
13 10 12 ax-mp ${⊢}{\cdot }_{{\mathrm{PwSer}}_{1}\left({R}\right)}={\cdot }_{{Y}}$
14 6 9 13 3eqtr2i ${⊢}{\cdot }_{{S}}={\cdot }_{{Y}}$
15 3 14 eqtr4i