Theorem gsumsubmcl

Description: Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 3-Jun-2019)

	Ref	Expression
Hypotheses	gsumsubmcl.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumsubmcl.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumsubmcl.a	$$⊢\phi \to A\in V$$
	gsumsubmcl.s	$$⊢\phi \to S\in \mathrm{SubMnd}\left(G\right)$$
	gsumsubmcl.f	$$⊢\phi \to F:A⟶S$$
	gsumsubmcl.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	gsumsubmcl	$$⊢\phi \to {\sum }_{G}F\in S$$

Proof

Step	Hyp	Ref	Expression
1		gsumsubmcl.z	$$⊢\underset{\dot{}}{0}=0_G$$
2		gsumsubmcl.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
3		gsumsubmcl.a	$$⊢\phi \to A\in V$$
4		gsumsubmcl.s	$$⊢\phi \to S\in \mathrm{SubMnd}\left(G\right)$$
5		gsumsubmcl.f	$$⊢\phi \to F:A⟶S$$
6		gsumsubmcl.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
7		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
8		cmnmnd	$$⊢G\in \mathrm{CMnd}\to G\in \mathrm{Mnd}$$
9	2 8	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
10		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
11	10	submss	$$⊢S\in \mathrm{SubMnd}\left(G\right)\to S\subseteq {\mathrm{Base}}_G$$
12	4 11	syl	$$⊢\phi \to S\subseteq {\mathrm{Base}}_G$$
13	5 12	fssd	$$⊢\phi \to F:A⟶{\mathrm{Base}}_G$$
14	10 7 2 13	cntzcmnf	$$⊢\phi \to \mathrm{ran}F\subseteq \mathrm{Cntz}\left(G\right)\left(\mathrm{ran}F\right)$$
15	1 7 9 3 4 5 14 6	gsumzsubmcl	$$⊢\phi \to {\sum }_{G}F\in S$$