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

Metamath Proof Explorer

Theorem mplsubg

Description: The set of polynomials is closed under addition, i.e. it is a subgroup of the set of power series. (Contributed by Mario Carneiro, 8-Jan-2015) (Proof shortened by AV, 16-Jul-2019)

Ref Expression
Hypotheses mplsubg.s 
|- S = ( I mPwSer R )
mplsubg.p 
|- P = ( I mPoly R )
mplsubg.u 
|- U = ( Base ` P )
mplsubg.i 
|- ( ph -> I e. W )
mplsubg.r 
|- ( ph -> R e. Grp )
Assertion mplsubg 
|- ( ph -> U e. ( SubGrp ` S ) )

Proof

Step Hyp Ref Expression
1 mplsubg.s 
 |-  S = ( I mPwSer R )
2 mplsubg.p 
 |-  P = ( I mPoly R )
3 mplsubg.u 
 |-  U = ( Base ` P )
4 mplsubg.i 
 |-  ( ph -> I e. W )
5 mplsubg.r 
 |-  ( ph -> R e. Grp )
6 eqid 
 |-  ( Base ` S ) = ( Base ` S )
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
9 0fi 
 |-  (/) e. Fin
10 9 a1i 
 |-  ( ph -> (/) e. Fin )
11 unfi 
 |-  ( ( x e. Fin /\ y e. Fin ) -> ( x u. y ) e. Fin )
12 11 adantl 
 |-  ( ( ph /\ ( x e. Fin /\ y e. Fin ) ) -> ( x u. y ) e. Fin )
13 ssfi 
 |-  ( ( x e. Fin /\ y C_ x ) -> y e. Fin )
14 13 adantl 
 |-  ( ( ph /\ ( x e. Fin /\ y C_ x ) ) -> y e. Fin )
15 1 2 3 4 mplsubglem2 
 |-  ( ph -> U = { g e. ( Base ` S ) | ( g supp ( 0g ` R ) ) e. Fin } )
16 1 6 7 8 4 10 12 14 15 5 mplsubglem 
 |-  ( ph -> U e. ( SubGrp ` S ) )