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	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
	ply1plusg.s	⊢ 𝑆 = ( 1o mPoly 𝑅 )
	ply1plusg.p	⊢ + = ( +g ‘ 𝑌 )
Assertion	ply1plusg	⊢ + = ( +g ‘ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ply1plusg.y	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2		ply1plusg.s	⊢ 𝑆 = ( 1o mPoly 𝑅 )
3		ply1plusg.p	⊢ + = ( +g ‘ 𝑌 )
4		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
5		eqid	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
6	2 4 5	mplplusg	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ ( 1o mPwSer 𝑅 ) )
7		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
8		eqid	⊢ ( +g ‘ ( PwSer1 ‘ 𝑅 ) ) = ( +g ‘ ( PwSer1 ‘ 𝑅 ) )
9	7 4 8	psr1plusg	⊢ ( +g ‘ ( PwSer1 ‘ 𝑅 ) ) = ( +g ‘ ( 1o mPwSer 𝑅 ) )
10		fvex	⊢ ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ V
11	1 7	ply1val	⊢ 𝑌 = ( ( PwSer1 ‘ 𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
12	11 8	ressplusg	⊢ ( ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ V → ( +g ‘ ( PwSer1 ‘ 𝑅 ) ) = ( +g ‘ 𝑌 ) )
13	10 12	ax-mp	⊢ ( +g ‘ ( PwSer1 ‘ 𝑅 ) ) = ( +g ‘ 𝑌 )
14	6 9 13	3eqtr2i	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑌 )
15	3 14	eqtr4i	⊢ + = ( +g ‘ 𝑆 )