Theorem mplring

Description: The polynomial ring is a ring. (Contributed by Mario Carneiro, 9-Jan-2015)

	Ref	Expression
Hypothesis	mplgrp.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
Assertion	mplring	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		mplgrp.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
3		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
4		simpl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝐼 ∈ 𝑉 )
5		simpr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
6	2 1 3 4 5	mplsubrg	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
7	1 2 3	mplval2	⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑃 ) )
8	7	subrgring	⊢ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) → 𝑃 ∈ Ring )
9	6 8	syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ Ring )