Theorem gsumzcl

Description: Closure of a finite group sum. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 1-Jun-2019)

	Ref	Expression
Hypotheses	gsumzcl.b	|- B = ( Base ` G )
	gsumzcl.0	|- .0. = ( 0g ` G )
	gsumzcl.z	|- Z = ( Cntz ` G )
	gsumzcl.g	|- ( ph -> G e. Mnd )
	gsumzcl.a	|- ( ph -> A e. V )
	gsumzcl.f	|- ( ph -> F : A --> B )
	gsumzcl.c	|- ( ph -> ran F C_ ( Z ` ran F ) )
	gsumzcl.w	|- ( ph -> F finSupp .0. )
Assertion	gsumzcl	|- ( ph -> ( G gsum F ) e. B )

Proof

Step	Hyp	Ref	Expression
1		gsumzcl.b	|- B = ( Base ` G )
2		gsumzcl.0	|- .0. = ( 0g ` G )
3		gsumzcl.z	|- Z = ( Cntz ` G )
4		gsumzcl.g	|- ( ph -> G e. Mnd )
5		gsumzcl.a	|- ( ph -> A e. V )
6		gsumzcl.f	|- ( ph -> F : A --> B )
7		gsumzcl.c	|- ( ph -> ran F C_ ( Z ` ran F ) )
8		gsumzcl.w	|- ( ph -> F finSupp .0. )
9	8	fsuppimpd	|- ( ph -> ( F supp .0. ) e. Fin )
10	1 2 3 4 5 6 7 9	gsumzcl2	|- ( ph -> ( G gsum F ) e. B )