Theorem mplcrng

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

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

Proof

Step	Hyp	Ref	Expression
1		mplgrp.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
3		simpl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝐼 ∈ 𝑉 )
4		simpr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing )
5	2 3 4	psrcrng	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( 𝐼 mPwSer 𝑅 ) ∈ CRing )
6		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
7		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
8	7	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
9	2 1 6 3 8	mplsubrg	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
10	1 2 6	mplval2	⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑃 ) )
11	10	subrgcrng	⊢ ( ( ( 𝐼 mPwSer 𝑅 ) ∈ CRing ∧ ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑃 ∈ CRing )
12	5 9 11	syl2anc	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ CRing )