This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. V /\ R e. Grp ) -> P e. 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 e. V /\ R e. Grp ) -> I e. V )
5 simpr 
 |-  ( ( I e. V /\ R e. Grp ) -> R e. Grp )
6 2 1 3 4 5 mplsubg 
 |-  ( ( I e. V /\ R e. Grp ) -> ( Base ` P ) e. ( SubGrp ` ( I mPwSer R ) ) )
7 1 2 3 mplval2 
 |-  P = ( ( I mPwSer R ) |`s ( Base ` P ) )
8 7 subggrp 
 |-  ( ( Base ` P ) e. ( SubGrp ` ( I mPwSer R ) ) -> P e. Grp )
9 6 8 syl 
 |-  ( ( I e. V /\ R e. Grp ) -> P e. Grp )