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 ) )