Metamath Proof Explorer

Theorem mplring

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

Ref Expression
Hypothesis mplgrp.p ⊢ P = I mPoly R
Assertion mplring ⊢ I ∈ V ∧ R ∈ Ring → P ∈ Ring

Proof

Step Hyp Ref Expression
1 mplgrp.p ⊢ P = I mPoly R
2 eqid ⊢ I mPwSer R = I mPwSer R
3 eqid ⊢ Base P = Base P
4 simpl ⊢ I ∈ V ∧ R ∈ Ring → I ∈ V
5 simpr ⊢ I ∈ V ∧ R ∈ Ring → R ∈ Ring
6 2 1 3 4 5 mplsubrg ⊢ I ∈ V ∧ R ∈ Ring → Base P ∈ SubRing ⁡ I mPwSer R
7 1 2 3 mplval2 ⊢ P = I mPwSer R ↾ 𝑠 Base P
8 7 subrgring ⊢ Base P ∈ SubRing ⁡ I mPwSer R → P ∈ Ring
9 6 8 syl ⊢ I ∈ V ∧ R ∈ Ring → P ∈ Ring