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	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
Assertion	ply1mulr	$$⊢\underset{\dot{}}{·}={\cdot }_S$$

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	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
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){\upharpoonright }_{𝑠}{\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	$$⊢\underset{\dot{}}{·}={\cdot }_S$$