Theorem gsumcl2

Description: Closure of a finite group sum. This theorem has a weaker hypothesis than gsumcl , because it is not required that F is a function (actually, the hypothesis always holds for any proper class F ). (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 )
	gsumcl2.w	|- ( ph -> ( F supp .0. ) e. Fin )
Assertion	gsumcl2	|- ( 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		gsumcl2.w	|- ( ph -> ( F supp .0. ) e. Fin )
7		eqid	|- ( Cntz ` G ) = ( Cntz ` G )
8		cmnmnd	|- ( G e. CMnd -> G e. Mnd )
9	3 8	syl	|- ( ph -> G e. Mnd )
10	1 7 3 5	cntzcmnf	|- ( ph -> ran F C_ ( ( Cntz ` G ) ` ran F ) )
11	1 2 7 9 4 5 10 6	gsumzcl2	|- ( ph -> ( G gsum F ) e. B )