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={\mathrm{Base}}_G$$
	gsumcl.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumcl.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumcl.a	$$⊢\phi \to A\in V$$
	gsumcl.f	$$⊢\phi \to F:A⟶B$$
	gsumcl2.w	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
Assertion	gsumcl2	$$⊢\phi \to {\sum }_{G}F\in B$$

Proof

Step	Hyp	Ref	Expression
1		gsumcl.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumcl.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumcl.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsumcl.a	$$⊢\phi \to A\in V$$
5		gsumcl.f	$$⊢\phi \to F:A⟶B$$
6		gsumcl2.w	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
7		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
8		cmnmnd	$$⊢G\in \mathrm{CMnd}\to G\in \mathrm{Mnd}$$
9	3 8	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
10	1 7 3 5	cntzcmnf	$$⊢\phi \to \mathrm{ran}F\subseteq \mathrm{Cntz}\left(G\right)\left(\mathrm{ran}F\right)$$
11	1 2 7 9 4 5 10 6	gsumzcl2	$$⊢\phi \to {\sum }_{G}F\in B$$