# Metamath Proof Explorer

## 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
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
Assertion gsumzsubmcl ${⊢}{\phi }\to {\sum }_{{G}}{F}\in {S}$

### Proof

Step Hyp Ref Expression
1 gsumzsubmcl.0
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
9 eqid ${⊢}{\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}={\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
10 eqid ${⊢}{0}_{\left({G}{↾}_{𝑠}{S}\right)}={0}_{\left({G}{↾}_{𝑠}{S}\right)}$
11 eqid ${⊢}\mathrm{Cntz}\left({G}{↾}_{𝑠}{S}\right)=\mathrm{Cntz}\left({G}{↾}_{𝑠}{S}\right)$
12 eqid ${⊢}{G}{↾}_{𝑠}{S}={G}{↾}_{𝑠}{S}$
13 12 submmnd ${⊢}{S}\in \mathrm{SubMnd}\left({G}\right)\to {G}{↾}_{𝑠}{S}\in \mathrm{Mnd}$
14 5 13 syl ${⊢}{\phi }\to {G}{↾}_{𝑠}{S}\in \mathrm{Mnd}$
15 12 submbas ${⊢}{S}\in \mathrm{SubMnd}\left({G}\right)\to {S}={\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
16 5 15 syl ${⊢}{\phi }\to {S}={\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
17 16 feq3d ${⊢}{\phi }\to \left({F}:{A}⟶{S}↔{F}:{A}⟶{\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}\right)$
18 6 17 mpbid ${⊢}{\phi }\to {F}:{A}⟶{\mathrm{Base}}_{\left({G}{↾}_{𝑠}{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}{↾}_{𝑠}{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}{↾}_{𝑠}{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}{↾}_{𝑠}{S}\right)\left(\mathrm{ran}{F}\right)$
24 12 1 subm0
25 5 24 syl
26 8 25 breqtrd ${⊢}{\phi }\to {finSupp}_{{0}_{\left({G}{↾}_{𝑠}{S}\right)}}\left({F}\right)$
27 9 10 11 14 4 18 23 26 gsumzcl ${⊢}{\phi }\to {\sum }_{{G}{↾}_{𝑠}{S}}{F}\in {\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
28 4 5 6 12 gsumsubm ${⊢}{\phi }\to {\sum }_{{G}}{F}={\sum }_{{G}{↾}_{𝑠}{S}}{F}$
29 27 28 16 3eltr4d ${⊢}{\phi }\to {\sum }_{{G}}{F}\in {S}$