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={\mathrm{Base}}_G$$
	gsumzcl.0	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumzcl.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	gsumzcl.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
	gsumzcl.a	$$⊢\phi \to A\in V$$
	gsumzcl.f	$$⊢\phi \to F:A⟶B$$
	gsumzcl.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
	gsumzcl.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	gsumzcl	$$⊢\phi \to {\sum }_{G}F\in B$$

Proof

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