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 0fin
 |-  (/) 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 ) )