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 mPoly R )
	mplplusg.s	|- S = ( I mPwSer R )
	mplmulr.n	|- .x. = ( .r ` Y )
Assertion	mplmulr	|- .x. = ( .r ` S )

Proof

Step	Hyp	Ref	Expression
1		mplplusg.y	|- Y = ( I mPoly R )
2		mplplusg.s	|- S = ( I mPwSer R )
3		mplmulr.n	|- .x. = ( .r ` Y )
4		fvex	|- ( Base ` Y ) e. _V
5		eqid	|- ( Base ` Y ) = ( Base ` Y )
6	1 2 5	mplval2	|- Y = ( S |`s ( Base ` Y ) )
7		eqid	|- ( .r ` S ) = ( .r ` S )
8	6 7	ressmulr	|- ( ( Base ` Y ) e. _V -> ( .r ` S ) = ( .r ` Y ) )
9	4 8	ax-mp	|- ( .r ` S ) = ( .r ` Y )
10	3 9	eqtr4i	|- .x. = ( .r ` S )