Metamath Proof Explorer

Theorem mplgrp

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

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

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 ∈ Grp → I ∈ V
5 simpr ⊢ I ∈ V ∧ R ∈ Grp → R ∈ Grp
6 2 1 3 4 5 mplsubg ⊢ I ∈ V ∧ R ∈ Grp → Base P ∈ SubGrp ⁡ I mPwSer R
7 1 2 3 mplval2 ⊢ P = I mPwSer R ↾ 𝑠 Base P
8 7 subggrp ⊢ Base P ∈ SubGrp ⁡ I mPwSer R → P ∈ Grp
9 6 8 syl ⊢ I ∈ V ∧ R ∈ Grp → P ∈ Grp