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	$⊢ φ \to I \in W$
		mplsubg.r	$⊢ φ \to R \in Grp$
	Assertion	mplsubg	$⊢ φ \to U \in 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	$⊢ φ \to I \in W$
5		mplsubg.r	$⊢ φ \to R \in Grp$
6		eqid	$⊢ {Base}_{S} = {Base}_{S}$
7		eqid	$⊢ 0_{R} = 0_{R}$
8		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
9		0fin	$⊢ \emptyset \in Fin$
10	9	a1i	$⊢ φ \to \emptyset \in Fin$
11		unfi	$⊢ (x \in Fin \land y \in Fin) \to x \cup y \in Fin$
12	11	adantl	$⊢ (φ \land (x \in Fin \land y \in Fin)) \to x \cup y \in Fin$
13		ssfi	$⊢ (x \in Fin \land y \subseteq x) \to y \in Fin$
14	13	adantl	$⊢ (φ \land (x \in Fin \land y \subseteq x)) \to y \in Fin$
15	1 2 3 4	mplsubglem2	$⊢ φ \to U = \{g \in {Base}_{S} \| g supp 0_{R} \in Fin\}$
16	1 6 7 8 4 10 12 14 15 5	mplsubglem	$⊢ φ \to U \in SubGrp (S)$