Metamath Proof Explorer


Theorem mplgrp

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

Ref Expression
Hypothesis mplgrp.p 𝑃 = ( 𝐼 mPoly 𝑅 )
Assertion mplgrp ( ( 𝐼𝑉𝑅 ∈ Grp ) → 𝑃 ∈ Grp )

Proof

Step Hyp Ref Expression
1 mplgrp.p 𝑃 = ( 𝐼 mPoly 𝑅 )
2 eqid ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
3 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
4 simpl ( ( 𝐼𝑉𝑅 ∈ Grp ) → 𝐼𝑉 )
5 simpr ( ( 𝐼𝑉𝑅 ∈ Grp ) → 𝑅 ∈ Grp )
6 2 1 3 4 5 mplsubg ( ( 𝐼𝑉𝑅 ∈ Grp ) → ( Base ‘ 𝑃 ) ∈ ( SubGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) )
7 1 2 3 mplval2 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑃 ) )
8 7 subggrp ( ( Base ‘ 𝑃 ) ∈ ( SubGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) → 𝑃 ∈ Grp )
9 6 8 syl ( ( 𝐼𝑉𝑅 ∈ Grp ) → 𝑃 ∈ Grp )