# Metamath Proof Explorer

## Theorem tgptsmscls

Description: A sum in a topological group is uniquely determined up to a coset of cls ( { 0 } ) , which is a normal subgroup by clsnsg , 0nsg . (Contributed by Mario Carneiro, 22-Sep-2015) (Proof shortened by AV, 24-Jul-2019)

Ref Expression
Hypotheses tgptsmscls.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
tgptsmscls.j ${⊢}{J}=\mathrm{TopOpen}\left({G}\right)$
tgptsmscls.1 ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
tgptsmscls.2 ${⊢}{\phi }\to {G}\in \mathrm{TopGrp}$
tgptsmscls.a ${⊢}{\phi }\to {A}\in {V}$
tgptsmscls.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
tgptsmscls.x ${⊢}{\phi }\to {X}\in \left({G}\mathrm{tsums}{F}\right)$
Assertion tgptsmscls ${⊢}{\phi }\to {G}\mathrm{tsums}{F}=\mathrm{cls}\left({J}\right)\left(\left\{{X}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 tgptsmscls.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 tgptsmscls.j ${⊢}{J}=\mathrm{TopOpen}\left({G}\right)$
3 tgptsmscls.1 ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
4 tgptsmscls.2 ${⊢}{\phi }\to {G}\in \mathrm{TopGrp}$
5 tgptsmscls.a ${⊢}{\phi }\to {A}\in {V}$
6 tgptsmscls.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
7 tgptsmscls.x ${⊢}{\phi }\to {X}\in \left({G}\mathrm{tsums}{F}\right)$
8 4 adantr ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {G}\in \mathrm{TopGrp}$
9 tgpgrp ${⊢}{G}\in \mathrm{TopGrp}\to {G}\in \mathrm{Grp}$
10 8 9 syl ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {G}\in \mathrm{Grp}$
11 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
12 11 0subg ${⊢}{G}\in \mathrm{Grp}\to \left\{{0}_{{G}}\right\}\in \mathrm{SubGrp}\left({G}\right)$
13 10 12 syl ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \left\{{0}_{{G}}\right\}\in \mathrm{SubGrp}\left({G}\right)$
14 2 clssubg ${⊢}\left({G}\in \mathrm{TopGrp}\wedge \left\{{0}_{{G}}\right\}\in \mathrm{SubGrp}\left({G}\right)\right)\to \mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\in \mathrm{SubGrp}\left({G}\right)$
15 8 13 14 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\in \mathrm{SubGrp}\left({G}\right)$
16 eqid ${⊢}{G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)={G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)$
17 1 16 eqger ${⊢}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\in \mathrm{SubGrp}\left({G}\right)\to \left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right)\mathrm{Er}{B}$
18 15 17 syl ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right)\mathrm{Er}{B}$
19 tgptps ${⊢}{G}\in \mathrm{TopGrp}\to {G}\in \mathrm{TopSp}$
20 4 19 syl ${⊢}{\phi }\to {G}\in \mathrm{TopSp}$
21 1 3 20 5 6 tsmscl ${⊢}{\phi }\to {G}\mathrm{tsums}{F}\subseteq {B}$
22 21 sselda ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {x}\in {B}$
23 21 7 sseldd ${⊢}{\phi }\to {X}\in {B}$
24 23 adantr ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {X}\in {B}$
25 eqid ${⊢}{-}_{{G}}={-}_{{G}}$
26 3 adantr ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {G}\in \mathrm{CMnd}$
27 5 adantr ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {A}\in {V}$
28 6 adantr ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {F}:{A}⟶{B}$
29 7 adantr ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {X}\in \left({G}\mathrm{tsums}{F}\right)$
30 simpr ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {x}\in \left({G}\mathrm{tsums}{F}\right)$
31 1 25 26 8 27 28 28 29 30 tsmssub ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {X}{-}_{{G}}{x}\in \left({G}\mathrm{tsums}\left({F}{{-}_{{G}}}_{f}{F}\right)\right)$
32 28 ffvelrnda ${⊢}\left(\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\wedge {k}\in {A}\right)\to {F}\left({k}\right)\in {B}$
33 28 feqmptd ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {F}=\left({k}\in {A}⟼{F}\left({k}\right)\right)$
34 27 32 32 33 33 offval2 ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {F}{{-}_{{G}}}_{f}{F}=\left({k}\in {A}⟼{F}\left({k}\right){-}_{{G}}{F}\left({k}\right)\right)$
35 10 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\wedge {k}\in {A}\right)\to {G}\in \mathrm{Grp}$
36 1 11 25 grpsubid ${⊢}\left({G}\in \mathrm{Grp}\wedge {F}\left({k}\right)\in {B}\right)\to {F}\left({k}\right){-}_{{G}}{F}\left({k}\right)={0}_{{G}}$
37 35 32 36 syl2anc ${⊢}\left(\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\wedge {k}\in {A}\right)\to {F}\left({k}\right){-}_{{G}}{F}\left({k}\right)={0}_{{G}}$
38 37 mpteq2dva ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \left({k}\in {A}⟼{F}\left({k}\right){-}_{{G}}{F}\left({k}\right)\right)=\left({k}\in {A}⟼{0}_{{G}}\right)$
39 34 38 eqtrd ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {F}{{-}_{{G}}}_{f}{F}=\left({k}\in {A}⟼{0}_{{G}}\right)$
40 39 oveq2d ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {G}\mathrm{tsums}\left({F}{{-}_{{G}}}_{f}{F}\right)={G}\mathrm{tsums}\left({k}\in {A}⟼{0}_{{G}}\right)$
41 8 19 syl ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {G}\in \mathrm{TopSp}$
42 1 11 grpidcl ${⊢}{G}\in \mathrm{Grp}\to {0}_{{G}}\in {B}$
43 10 42 syl ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {0}_{{G}}\in {B}$
44 43 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\wedge {k}\in {A}\right)\to {0}_{{G}}\in {B}$
45 44 fmpttd ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \left({k}\in {A}⟼{0}_{{G}}\right):{A}⟶{B}$
46 fconstmpt ${⊢}{A}×\left\{{0}_{{G}}\right\}=\left({k}\in {A}⟼{0}_{{G}}\right)$
47 fvexd ${⊢}{\phi }\to {0}_{{G}}\in \mathrm{V}$
48 5 47 fczfsuppd ${⊢}{\phi }\to {finSupp}_{{0}_{{G}}}\left(\left({A}×\left\{{0}_{{G}}\right\}\right)\right)$
49 48 adantr ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {finSupp}_{{0}_{{G}}}\left(\left({A}×\left\{{0}_{{G}}\right\}\right)\right)$
50 46 49 eqbrtrrid ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {finSupp}_{{0}_{{G}}}\left(\left({k}\in {A}⟼{0}_{{G}}\right)\right)$
51 1 11 26 41 27 45 50 2 tsmsgsum ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {G}\mathrm{tsums}\left({k}\in {A}⟼{0}_{{G}}\right)=\mathrm{cls}\left({J}\right)\left(\left\{\underset{{k}\in {A}}{{\sum }_{{G}}}{0}_{{G}}\right\}\right)$
52 cmnmnd ${⊢}{G}\in \mathrm{CMnd}\to {G}\in \mathrm{Mnd}$
53 26 52 syl ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {G}\in \mathrm{Mnd}$
54 11 gsumz ${⊢}\left({G}\in \mathrm{Mnd}\wedge {A}\in {V}\right)\to \underset{{k}\in {A}}{{\sum }_{{G}}}{0}_{{G}}={0}_{{G}}$
55 53 27 54 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \underset{{k}\in {A}}{{\sum }_{{G}}}{0}_{{G}}={0}_{{G}}$
56 55 sneqd ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \left\{\underset{{k}\in {A}}{{\sum }_{{G}}}{0}_{{G}}\right\}=\left\{{0}_{{G}}\right\}$
57 56 fveq2d ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \mathrm{cls}\left({J}\right)\left(\left\{\underset{{k}\in {A}}{{\sum }_{{G}}}{0}_{{G}}\right\}\right)=\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)$
58 40 51 57 3eqtrd ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {G}\mathrm{tsums}\left({F}{{-}_{{G}}}_{f}{F}\right)=\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)$
59 31 58 eleqtrd ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {X}{-}_{{G}}{x}\in \mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)$
60 isabl ${⊢}{G}\in \mathrm{Abel}↔\left({G}\in \mathrm{Grp}\wedge {G}\in \mathrm{CMnd}\right)$
61 10 26 60 sylanbrc ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {G}\in \mathrm{Abel}$
62 1 subgss ${⊢}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\in \mathrm{SubGrp}\left({G}\right)\to \mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\subseteq {B}$
63 15 62 syl ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\subseteq {B}$
64 1 25 16 eqgabl ${⊢}\left({G}\in \mathrm{Abel}\wedge \mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\subseteq {B}\right)\to \left({x}\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right){X}↔\left({x}\in {B}\wedge {X}\in {B}\wedge {X}{-}_{{G}}{x}\in \mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right)\right)$
65 61 63 64 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \left({x}\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right){X}↔\left({x}\in {B}\wedge {X}\in {B}\wedge {X}{-}_{{G}}{x}\in \mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right)\right)$
66 22 24 59 65 mpbir3and ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {x}\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right){X}$
67 18 66 ersym ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {X}\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right){x}$
68 16 releqg ${⊢}\mathrm{Rel}\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right)$
69 relelec ${⊢}\mathrm{Rel}\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right)\to \left({x}\in \left[{X}\right]\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right)↔{X}\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right){x}\right)$
70 68 69 ax-mp ${⊢}{x}\in \left[{X}\right]\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right)↔{X}\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right){x}$
71 67 70 sylibr ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {x}\in \left[{X}\right]\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right)$
72 eqid ${⊢}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)=\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)$
73 1 2 11 16 72 snclseqg ${⊢}\left({G}\in \mathrm{TopGrp}\wedge {X}\in {B}\right)\to \left[{X}\right]\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right)=\mathrm{cls}\left({J}\right)\left(\left\{{X}\right\}\right)$
74 8 24 73 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \left[{X}\right]\left({G}{~}_{\mathit{QG}}\mathrm{cls}\left({J}\right)\left(\left\{{0}_{{G}}\right\}\right)\right)=\mathrm{cls}\left({J}\right)\left(\left\{{X}\right\}\right)$
75 71 74 eleqtrd ${⊢}\left({\phi }\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {x}\in \mathrm{cls}\left({J}\right)\left(\left\{{X}\right\}\right)$
76 75 ex ${⊢}{\phi }\to \left({x}\in \left({G}\mathrm{tsums}{F}\right)\to {x}\in \mathrm{cls}\left({J}\right)\left(\left\{{X}\right\}\right)\right)$
77 76 ssrdv ${⊢}{\phi }\to {G}\mathrm{tsums}{F}\subseteq \mathrm{cls}\left({J}\right)\left(\left\{{X}\right\}\right)$
78 1 2 3 20 5 6 7 tsmscls ${⊢}{\phi }\to \mathrm{cls}\left({J}\right)\left(\left\{{X}\right\}\right)\subseteq {G}\mathrm{tsums}{F}$
79 77 78 eqssd ${⊢}{\phi }\to {G}\mathrm{tsums}{F}=\mathrm{cls}\left({J}\right)\left(\left\{{X}\right\}\right)$