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 φ I W
mplsubg.r φ R Grp
Assertion mplsubg φ U 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 φ I W
5 mplsubg.r φ R Grp
6 eqid Base S = Base S
7 eqid 0 R = 0 R
8 eqid f 0 I | f -1 Fin = f 0 I | f -1 Fin
9 0fin Fin
10 9 a1i φ Fin
11 unfi x Fin y Fin x y Fin
12 11 adantl φ x Fin y Fin x y Fin
13 ssfi x Fin y x y Fin
14 13 adantl φ x Fin y x y Fin
15 1 2 3 4 mplsubglem2 φ U = g Base S | g supp 0 R Fin
16 1 6 7 8 4 10 12 14 15 5 mplsubglem φ U SubGrp S