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 = ( Base ` G )
	gsummptcl.g	|- ( ph -> G e. CMnd )
	gsummptcl.n	|- ( ph -> N e. Fin )
	gsummptcl.e	|- ( ph -> A. i e. N X e. B )
Assertion	gsummptcl	|- ( ph -> ( G gsum ( i e. N |-> X ) ) e. B )

Proof

Step	Hyp	Ref	Expression
1		gsummptcl.b	|- B = ( Base ` G )
2		gsummptcl.g	|- ( ph -> G e. CMnd )
3		gsummptcl.n	|- ( ph -> N e. Fin )
4		gsummptcl.e	|- ( ph -> A. i e. N X e. B )
5		eqid	|- ( 0g ` G ) = ( 0g ` G )
6		eqid	|- ( i e. N |-> X ) = ( i e. N |-> X )
7	6	fmpt	|- ( A. i e. N X e. B <-> ( i e. N |-> X ) : N --> B )
8	4 7	sylib	|- ( ph -> ( i e. N |-> X ) : N --> B )
9	6	fnmpt	|- ( A. i e. N X e. B -> ( i e. N |-> X ) Fn N )
10	4 9	syl	|- ( ph -> ( i e. N |-> X ) Fn N )
11		fvexd	|- ( ph -> ( 0g ` G ) e. _V )
12	10 3 11	fndmfifsupp	|- ( ph -> ( i e. N |-> X ) finSupp ( 0g ` G ) )
13	1 5 2 3 8 12	gsumcl	|- ( ph -> ( G gsum ( i e. N |-> X ) ) e. B )