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	⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
	mplplusg.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	mplmulr.n	⊢ · = ( .r ‘ 𝑌 )
Assertion	mplmulr	⊢ · = ( .r ‘ 𝑆 )

Proof

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