Theorem gsumzsubmcl

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

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

Proof

Step	Hyp	Ref	Expression
1		gsumzsubmcl.0	$$⊢\underset{\dot{}}{0}=0_G$$
2		gsumzsubmcl.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
3		gsumzsubmcl.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
4		gsumzsubmcl.a	$$⊢\phi \to A\in V$$
5		gsumzsubmcl.s	$$⊢\phi \to S\in \mathrm{SubMnd}\left(G\right)$$
6		gsumzsubmcl.f	$$⊢\phi \to F:A⟶S$$
7		gsumzsubmcl.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
8		gsumzsubmcl.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
9		eqid	$$⊢{\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
10		eqid	$$⊢0_{\left(G{\upharpoonright }_{𝑠}S\right)}=0_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
11		eqid	$$⊢\mathrm{Cntz}\left(G{\upharpoonright }_{𝑠}S\right)=\mathrm{Cntz}\left(G{\upharpoonright }_{𝑠}S\right)$$
12		eqid	$$⊢G{\upharpoonright }_{𝑠}S=G{\upharpoonright }_{𝑠}S$$
13	12	submmnd	$$⊢S\in \mathrm{SubMnd}\left(G\right)\to G{\upharpoonright }_{𝑠}S\in \mathrm{Mnd}$$
14	5 13	syl	$$⊢\phi \to G{\upharpoonright }_{𝑠}S\in \mathrm{Mnd}$$
15	12	submbas	$$⊢S\in \mathrm{SubMnd}\left(G\right)\to S={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
16	5 15	syl	$$⊢\phi \to S={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
17	16	feq3d	$$⊢\phi \to \left(F:A⟶S\leftrightarrow F:A⟶{\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}\right)$$
18	6 17	mpbid	$$⊢\phi \to F:A⟶{\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
19	6	frnd	$$⊢\phi \to \mathrm{ran}F\subseteq S$$
20	7 19	ssind	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)\cap S$$
21	12 2 11	resscntz	$$⊢\left(S\in \mathrm{SubMnd}\left(G\right)\wedge \mathrm{ran}F\subseteq S\right)\to \mathrm{Cntz}\left(G{\upharpoonright }_{𝑠}S\right)\left(\mathrm{ran}F\right)=Z\left(\mathrm{ran}F\right)\cap S$$
22	5 19 21	syl2anc	$$⊢\phi \to \mathrm{Cntz}\left(G{\upharpoonright }_{𝑠}S\right)\left(\mathrm{ran}F\right)=Z\left(\mathrm{ran}F\right)\cap S$$
23	20 22	sseqtrrd	$$⊢\phi \to \mathrm{ran}F\subseteq \mathrm{Cntz}\left(G{\upharpoonright }_{𝑠}S\right)\left(\mathrm{ran}F\right)$$
24	12 1	subm0	$$⊢S\in \mathrm{SubMnd}\left(G\right)\to \underset{\dot{}}{0}=0_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
25	5 24	syl	$$⊢\phi \to \underset{\dot{}}{0}=0_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
26	8 25	breqtrd	$$⊢\phi \to {finSupp}_{0_{\left(G{\upharpoonright }_{𝑠}S\right)}}\left(F\right)$$
27	9 10 11 14 4 18 23 26	gsumzcl	$$⊢\phi \to {\sum }_{G{\upharpoonright }_{𝑠}S}F\in {\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
28	4 5 6 12	gsumsubm	$$⊢\phi \to {\sum }_{G}F={\sum }_{G{\upharpoonright }_{𝑠}S}F$$
29	27 28 16	3eltr4d	$$⊢\phi \to {\sum }_{G}F\in S$$