Metamath Proof Explorer

Theorem mplcrng

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

Ref Expression
Hypothesis mplgrp.p 
|- P = ( I mPoly R )
Assertion mplcrng 
|- ( ( I e. V /\ R e. CRing ) -> P e. CRing )

Proof

Step Hyp Ref Expression
1 mplgrp.p 
 |-  P = ( I mPoly R )
2 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
3 simpl 
 |-  ( ( I e. V /\ R e. CRing ) -> I e. V )
4 simpr 
 |-  ( ( I e. V /\ R e. CRing ) -> R e. CRing )
5 2 3 4 psrcrng 
 |-  ( ( I e. V /\ R e. CRing ) -> ( I mPwSer R ) e. CRing )
6 eqid 
 |-  ( Base ` P ) = ( Base ` P )
7 crngring 
 |-  ( R e. CRing -> R e. Ring )
8 7 adantl 
 |-  ( ( I e. V /\ R e. CRing ) -> R e. Ring )
9 2 1 6 3 8 mplsubrg 
 |-  ( ( I e. V /\ R e. CRing ) -> ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) )
10 1 2 6 mplval2 
 |-  P = ( ( I mPwSer R ) |`s ( Base ` P ) )
11 10 subrgcrng 
 |-  ( ( ( I mPwSer R ) e. CRing /\ ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) ) -> P e. CRing )
12 5 9 11 syl2anc 
 |-  ( ( I e. V /\ R e. CRing ) -> P e. CRing )