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 ∈ V ∧ R ∈ CRing → P ∈ CRing

Proof

Step Hyp Ref Expression
1 mplgrp.p ⊢ P = I mPoly R
2 eqid ⊢ I mPwSer R = I mPwSer R
3 simpl ⊢ I ∈ V ∧ R ∈ CRing → I ∈ V
4 simpr ⊢ I ∈ V ∧ R ∈ CRing → R ∈ CRing
5 2 3 4 psrcrng ⊢ I ∈ V ∧ R ∈ CRing → I mPwSer R ∈ CRing
6 eqid ⊢ Base P = Base P
7 crngring ⊢ R ∈ CRing → R ∈ Ring
8 7 adantl ⊢ I ∈ V ∧ R ∈ CRing → R ∈ Ring
9 2 1 6 3 8 mplsubrg ⊢ I ∈ V ∧ R ∈ CRing → Base P ∈ SubRing ⁡ I mPwSer R
10 1 2 6 mplval2 ⊢ P = I mPwSer R ↾ 𝑠 Base P
11 10 subrgcrng ⊢ I mPwSer R ∈ CRing ∧ Base P ∈ SubRing ⁡ I mPwSer R → P ∈ CRing
12 5 9 11 syl2anc ⊢ I ∈ V ∧ R ∈ CRing → P ∈ CRing