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	⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
	mplplusg.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	mplplusg.p	⊢ + = ( +g ‘ 𝑌 )
Assertion	mplplusg	⊢ + = ( +g ‘ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		mplplusg.y	⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
2		mplplusg.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
3		mplplusg.p	⊢ + = ( +g ‘ 𝑌 )
4		fvex	⊢ ( Base ‘ 𝑌 ) ∈ V
5		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
6	1 2 5	mplval2	⊢ 𝑌 = ( 𝑆 ↾s ( Base ‘ 𝑌 ) )
7		eqid	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
8	6 7	ressplusg	⊢ ( ( Base ‘ 𝑌 ) ∈ V → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑌 ) )
9	4 8	ax-mp	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑌 )
10	3 9	eqtr4i	⊢ + = ( +g ‘ 𝑆 )