Theorem gsummptcl

Description: Closure of a finite group sum over a finite set as map. (Contributed by AV, 29-Dec-2018)

	Ref	Expression
Hypotheses	gsummptcl.b	$$⊢B={\mathrm{Base}}_G$$
	gsummptcl.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsummptcl.n	$$⊢\phi \to N\in \mathrm{Fin}$$
	gsummptcl.e	$$⊢\phi \to \forall i\in NX\in B$$
Assertion	gsummptcl	$$⊢\phi \to \underset{i\in N}{{\sum }_G}X\in B$$

Proof

Step	Hyp	Ref	Expression
1		gsummptcl.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummptcl.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
3		gsummptcl.n	$$⊢\phi \to N\in \mathrm{Fin}$$
4		gsummptcl.e	$$⊢\phi \to \forall i\in NX\in B$$
5		eqid	$$⊢0_G=0_G$$
6		eqid	$$⊢\left(i\in N⟼X\right)=\left(i\in N⟼X\right)$$
7	6	fmpt	$$⊢\forall i\in NX\in B\leftrightarrow \left(i\in N⟼X\right):N⟶B$$
8	4 7	sylib	$$⊢\phi \to \left(i\in N⟼X\right):N⟶B$$
9	6	fnmpt	$$⊢\forall i\in NX\in B\to \left(i\in N⟼X\right)FnN$$
10	4 9	syl	$$⊢\phi \to \left(i\in N⟼X\right)FnN$$
11		fvexd	$$⊢\phi \to 0_G\in \mathrm{V}$$
12	10 3 11	fndmfifsupp	$$⊢\phi \to {finSupp}_{0_G}\left(\left(i\in N⟼X\right)\right)$$
13	1 5 2 3 8 12	gsumcl	$$⊢\phi \to \underset{i\in N}{{\sum }_G}X\in B$$