Theorem ply1plusg

Description: Value of addition 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 = ( Poly1 ` R )
	ply1plusg.s	|- S = ( 1o mPoly R )
	ply1plusg.p	|- .+ = ( +g ` Y )
Assertion	ply1plusg	|- .+ = ( +g ` S )

Proof

Step	Hyp	Ref	Expression
1		ply1plusg.y	|- Y = ( Poly1 ` R )
2		ply1plusg.s	|- S = ( 1o mPoly R )
3		ply1plusg.p	|- .+ = ( +g ` Y )
4		eqid	|- ( 1o mPwSer R ) = ( 1o mPwSer R )
5		eqid	|- ( +g ` S ) = ( +g ` S )
6	2 4 5	mplplusg	|- ( +g ` S ) = ( +g ` ( 1o mPwSer R ) )
7		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
8		eqid	|- ( +g ` ( PwSer1 ` R ) ) = ( +g ` ( PwSer1 ` R ) )
9	7 4 8	psr1plusg	|- ( +g ` ( PwSer1 ` R ) ) = ( +g ` ( 1o mPwSer R ) )
10		fvex	|- ( Base ` ( 1o mPoly R ) ) e. _V
11	1 7	ply1val	|- Y = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
12	11 8	ressplusg	|- ( ( Base ` ( 1o mPoly R ) ) e. _V -> ( +g ` ( PwSer1 ` R ) ) = ( +g ` Y ) )
13	10 12	ax-mp	|- ( +g ` ( PwSer1 ` R ) ) = ( +g ` Y )
14	6 9 13	3eqtr2i	|- ( +g ` S ) = ( +g ` Y )
15	3 14	eqtr4i	|- .+ = ( +g ` S )