Theorem gsumcl

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

	Ref	Expression
Hypotheses	gsumcl.b	|- B = ( Base ` G )
	gsumcl.z	|- .0. = ( 0g ` G )
	gsumcl.g	|- ( ph -> G e. CMnd )
	gsumcl.a	|- ( ph -> A e. V )
	gsumcl.f	|- ( ph -> F : A --> B )
	gsumcl.w	|- ( ph -> F finSupp .0. )
Assertion	gsumcl	|- ( ph -> ( G gsum F ) e. B )

Proof

Step	Hyp	Ref	Expression
1		gsumcl.b	|- B = ( Base ` G )
2		gsumcl.z	|- .0. = ( 0g ` G )
3		gsumcl.g	|- ( ph -> G e. CMnd )
4		gsumcl.a	|- ( ph -> A e. V )
5		gsumcl.f	|- ( ph -> F : A --> B )
6		gsumcl.w	|- ( ph -> F finSupp .0. )
7	6	fsuppimpd	|- ( ph -> ( F supp .0. ) e. Fin )
8	1 2 3 4 5 7	gsumcl2	|- ( ph -> ( G gsum F ) e. B )