Theorem mplplusg

Description: Value of addition 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 )
	mplplusg.p	|- .+ = ( +g ` Y )
Assertion	mplplusg	|- .+ = ( +g ` S )

Proof

Step	Hyp	Ref	Expression
1		mplplusg.y	|- Y = ( I mPoly R )
2		mplplusg.s	|- S = ( I mPwSer R )
3		mplplusg.p	|- .+ = ( +g ` 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	|- ( +g ` S ) = ( +g ` S )
8	6 7	ressplusg	|- ( ( Base ` Y ) e. _V -> ( +g ` S ) = ( +g ` Y ) )
9	4 8	ax-mp	|- ( +g ` S ) = ( +g ` Y )
10	3 9	eqtr4i	|- .+ = ( +g ` S )