Theorem mplmulr

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

	Ref	Expression
Hypotheses	mplplusg.y	$$⊢Y=I\mathrm{mPoly}R$$
	mplplusg.s	$$⊢S=I\mathrm{mPwSer}R$$
	mplmulr.n	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
Assertion	mplmulr	$$⊢\underset{\dot{}}{·}={\cdot }_S$$

Proof

Step	Hyp	Ref	Expression
1		mplplusg.y	$$⊢Y=I\mathrm{mPoly}R$$
2		mplplusg.s	$$⊢S=I\mathrm{mPwSer}R$$
3		mplmulr.n	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
4		fvex	$$⊢{\mathrm{Base}}_Y\in \mathrm{V}$$
5		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
6	1 2 5	mplval2	$$⊢Y=S{\upharpoonright }_{𝑠}{\mathrm{Base}}_Y$$
7		eqid	$$⊢{\cdot }_S={\cdot }_S$$
8	6 7	ressmulr	$$⊢{\mathrm{Base}}_Y\in \mathrm{V}\to {\cdot }_S={\cdot }_Y$$
9	4 8	ax-mp	$$⊢{\cdot }_S={\cdot }_Y$$
10	3 9	eqtr4i	$$⊢\underset{\dot{}}{·}={\cdot }_S$$