Theorem tgptsmscls 20760

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

Hypotheses

Ref	Expression
tgptsmscls.b	|- B = ( Base ` G )
tgptsmscls.j	|- J = ( TopOpen ` G )
tgptsmscls.1	|- ( ph -> G e. CMnd )
tgptsmscls.2	|- ( ph -> G e. TopGrp )
tgptsmscls.a	|- ( ph -> A e. V )
tgptsmscls.f	|- ( ph -> F : A --> B )
tgptsmscls.x	|- ( ph -> X e. ( G tsums F ) )

Assertion

Ref	Expression
tgptsmscls	|- ( ph -> ( G tsums F ) = ( ( cls ` J ) ` { X } ) )

Proof of Theorem tgptsmscls

Dummy variables k x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tgptsmscls.2	. . . . . . . . . 10 |- ( ph -> G e. TopGrp )
2	1	adantr 463	. . . . . . . . 9 |- ( ( ph /\ x e. ( G tsums F ) ) -> G e. TopGrp )
3		tgpgrp 20685	. . . . . . . . . . 11 |- ( G e. TopGrp -> G e. Grp )
4	2, 3	syl 16	. . . . . . . . . 10 |- ( ( ph /\ x e. ( G tsums F ) ) -> G e. Grp )
5		eqid 2396	. . . . . . . . . . 11 |- ( 0g ` G ) = ( 0g ` G )
6	5	0subg 16366	. . . . . . . . . 10 |- ( G e. Grp -> { ( 0g ` G ) } e. (SubGrp ` G ) )
7	4, 6	syl 16	. . . . . . . . 9 |- ( ( ph /\ x e. ( G tsums F ) ) -> { ( 0g ` G ) } e. (SubGrp ` G ) )
8		tgptsmscls.j	. . . . . . . . . 10 |- J = ( TopOpen ` G )
9	8	clssubg 20715	. . . . . . . . 9 |- ( ( G e. TopGrp /\ { ( 0g ` G ) } e. (SubGrp ` G ) ) -> ( ( cls ` J ) ` { ( 0g ` G ) } ) e. (SubGrp ` G ) )
10	2, 7, 9	syl2anc 659	. . . . . . . 8 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( ( cls ` J ) ` { ( 0g ` G ) } ) e. (SubGrp ` G ) )
11		tgptsmscls.b	. . . . . . . . 9 |- B = ( Base ` G )
12		eqid 2396	. . . . . . . . 9 |- ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) = ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) )
13	11, 12	eqger 16391	. . . . . . . 8 |- ( ( ( cls ` J ) ` { ( 0g ` G ) } ) e. (SubGrp ` G ) -> ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) Er B )
14	10, 13	syl 16	. . . . . . 7 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) Er B )
15		tgptsmscls.1	. . . . . . . . . 10 |- ( ph -> G e. CMnd )
16		tgptps 20687	. . . . . . . . . . 11 |- ( G e. TopGrp -> G e. TopSp )
17	1, 16	syl 16	. . . . . . . . . 10 |- ( ph -> G e. TopSp )
18		tgptsmscls.a	. . . . . . . . . 10 |- ( ph -> A e. V )
19		tgptsmscls.f	. . . . . . . . . 10 |- ( ph -> F : A --> B )
20	11, 15, 17, 18, 19	tsmscl 20741	. . . . . . . . 9 |- ( ph -> ( G tsums F ) C_ B )
21	20	sselda 3434	. . . . . . . 8 |- ( ( ph /\ x e. ( G tsums F ) ) -> x e. B )
22		tgptsmscls.x	. . . . . . . . . 10 |- ( ph -> X e. ( G tsums F ) )
23	20, 22	sseldd 3435	. . . . . . . . 9 |- ( ph -> X e. B )
24	23	adantr 463	. . . . . . . 8 |- ( ( ph /\ x e. ( G tsums F ) ) -> X e. B )
25		eqid 2396	. . . . . . . . . 10 |- ( -g ` G ) = ( -g ` G )
26	15	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ x e. ( G tsums F ) ) -> G e. CMnd )
27	18	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ x e. ( G tsums F ) ) -> A e. V )
28	19	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ x e. ( G tsums F ) ) -> F : A --> B )
29	22	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ x e. ( G tsums F ) ) -> X e. ( G tsums F ) )
30		simpr 459	. . . . . . . . . 10 |- ( ( ph /\ x e. ( G tsums F ) ) -> x e. ( G tsums F ) )
31	11, 25, 26, 2, 27, 28, 28, 29, 30	tsmssub 20759	. . . . . . . . 9 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( X ( -g ` G ) x ) e. ( G tsums ( F oF ( -g ` G ) F ) ) )
32	28	ffvelrnda 5950	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( G tsums F ) ) /\ k e. A ) -> ( F ` k ) e. B )
33	28	feqmptd 5844	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( G tsums F ) ) -> F = ( k e. A |-> ( F ` k ) ) )
34	27, 32, 32, 33, 33	offval2 6477	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( F oF ( -g ` G ) F ) = ( k e. A |-> ( ( F ` k ) ( -g ` G ) ( F ` k ) ) ) )
35	4	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( G tsums F ) ) /\ k e. A ) -> G e. Grp )
36	11, 5, 25	grpsubid 16262	. . . . . . . . . . . . . 14 |- ( ( G e. Grp /\ ( F ` k ) e. B ) -> ( ( F ` k ) ( -g ` G ) ( F ` k ) ) = ( 0g ` G ) )
37	35, 32, 36	syl2anc 659	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( G tsums F ) ) /\ k e. A ) -> ( ( F ` k ) ( -g ` G ) ( F ` k ) ) = ( 0g ` G ) )
38	37	mpteq2dva 4470	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( k e. A |-> ( ( F ` k ) ( -g ` G ) ( F ` k ) ) ) = ( k e. A |-> ( 0g ` G ) ) )
39	34, 38	eqtrd 2437	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( F oF ( -g ` G ) F ) = ( k e. A |-> ( 0g ` G ) ) )
40	39	oveq2d 6234	. . . . . . . . . 10 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( G tsums ( F oF ( -g ` G ) F ) ) = ( G tsums ( k e. A |-> ( 0g ` G ) ) ) )
41	2, 16	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( G tsums F ) ) -> G e. TopSp )
42	11, 5	grpidcl 16218	. . . . . . . . . . . . . 14 |- ( G e. Grp -> ( 0g ` G ) e. B )
43	4, 42	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( 0g ` G ) e. B )
44	43	adantr 463	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( G tsums F ) ) /\ k e. A ) -> ( 0g ` G ) e. B )
45		eqid 2396	. . . . . . . . . . . 12 |- ( k e. A |-> ( 0g ` G ) ) = ( k e. A |-> ( 0g ` G ) )
46	44, 45	fmptd 5974	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( k e. A |-> ( 0g ` G ) ) : A --> B )
47		fconstmpt 4974	. . . . . . . . . . . 12 |- ( A X. { ( 0g ` G ) } ) = ( k e. A |-> ( 0g ` G ) )
48		fvex 5801	. . . . . . . . . . . . . . 15 |- ( 0g ` G ) e. _V
49	48	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 0g ` G ) e. _V )
50	18, 49	fczfsuppd 7784	. . . . . . . . . . . . 13 |- ( ph -> ( A X. { ( 0g ` G ) } ) finSupp ( 0g ` G ) )
51	50	adantr 463	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( A X. { ( 0g ` G ) } ) finSupp ( 0g ` G ) )
52	47, 51	syl5eqbrr 4418	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( k e. A |-> ( 0g ` G ) ) finSupp ( 0g ` G ) )
53	11, 5, 26, 41, 27, 46, 52, 8	tsmsgsum 20745	. . . . . . . . . 10 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( G tsums ( k e. A |-> ( 0g ` G ) ) ) = ( ( cls ` J ) ` { ( G gsumg ( k e. A |-> ( 0g ` G ) ) ) } ) )
54		cmnmnd 16953	. . . . . . . . . . . . . 14 |- ( G e. CMnd -> G e. Mnd )
55	26, 54	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( G tsums F ) ) -> G e. Mnd )
56	5	gsumz 16145	. . . . . . . . . . . . 13 |- ( ( G e. Mnd /\ A e. V ) -> ( G gsumg ( k e. A |-> ( 0g ` G ) ) ) = ( 0g ` G ) )
57	55, 27, 56	syl2anc 659	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( G gsumg ( k e. A |-> ( 0g ` G ) ) ) = ( 0g ` G ) )
58	57	sneqd 3973	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( G tsums F ) ) -> { ( G gsumg ( k e. A |-> ( 0g ` G ) ) ) } = { ( 0g ` G ) } )
59	58	fveq2d 5795	. . . . . . . . . 10 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( ( cls ` J ) ` { ( G gsumg ( k e. A |-> ( 0g ` G ) ) ) } ) = ( ( cls ` J ) ` { ( 0g ` G ) } ) )
60	40, 53, 59	3eqtrd 2441	. . . . . . . . 9 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( G tsums ( F oF ( -g ` G ) F ) ) = ( ( cls ` J ) ` { ( 0g ` G ) } ) )
61	31, 60	eleqtrd 2486	. . . . . . . 8 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( X ( -g ` G ) x ) e. ( ( cls ` J ) ` { ( 0g ` G ) } ) )
62		isabl 16942	. . . . . . . . . 10 |- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
63	4, 26, 62	sylanbrc 662	. . . . . . . . 9 |- ( ( ph /\ x e. ( G tsums F ) ) -> G e. Abel )
64	11	subgss 16342	. . . . . . . . . 10 |- ( ( ( cls ` J ) ` { ( 0g ` G ) } ) e. (SubGrp ` G ) -> ( ( cls ` J ) ` { ( 0g ` G ) } ) C_ B )
65	10, 64	syl 16	. . . . . . . . 9 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( ( cls ` J ) ` { ( 0g ` G ) } ) C_ B )
66	11, 25, 12	eqgabl 16983	. . . . . . . . 9 |- ( ( G e. Abel /\ ( ( cls ` J ) ` { ( 0g ` G ) } ) C_ B ) -> ( x ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) X <-> ( x e. B /\ X e. B /\ ( X ( -g ` G ) x ) e. ( ( cls ` J ) ` { ( 0g ` G ) } ) ) ) )
67	63, 65, 66	syl2anc 659	. . . . . . . 8 |- ( ( ph /\ x e. ( G tsums F ) ) -> ( x ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) X <-> ( x e. B /\ X e. B /\ ( X ( -g ` G ) x ) e. ( ( cls ` J ) ` { ( 0g ` G ) } ) ) ) )
68	21, 24, 61, 67	mpbir3and 1177	. . . . . . 7 |- ( ( ph /\ x e. ( G tsums F ) ) -> x ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) X )
69	14, 68	ersym 7263	. . . . . 6 |- ( ( ph /\ x e. ( G tsums F ) ) -> X ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) x )
70	12	releqg 16388	. . . . . . 7 |- Rel ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) )
71		relelec 7292	. . . . . . 7 |- ( Rel ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) -> ( x e. [ X ] ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) <-> X ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) x ) )
72	70, 71	ax-mp 5	. . . . . 6 |- ( x e. [ X ] ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) <-> X ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) x )
73	69, 72	sylibr 212	. . . . 5 |- ( ( ph /\ x e. ( G tsums F ) ) -> x e. [ X ] ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) )
74		eqid 2396	. . . . . . 7 |- ( ( cls ` J ) ` { ( 0g ` G ) } ) = ( ( cls ` J ) ` { ( 0g ` G ) } )
75	11, 8, 5, 12, 74	snclseqg 20722	. . . . . 6 |- ( ( G e. TopGrp /\ X e. B ) -> [ X ] ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) = ( ( cls ` J ) ` { X } ) )
76	2, 24, 75	syl2anc 659	. . . . 5 |- ( ( ph /\ x e. ( G tsums F ) ) -> [ X ] ( G ~QG ( ( cls ` J ) ` { ( 0g ` G ) } ) ) = ( ( cls ` J ) ` { X } ) )
77	73, 76	eleqtrd 2486	. . . 4 |- ( ( ph /\ x e. ( G tsums F ) ) -> x e. ( ( cls ` J ) ` { X } ) )
78	77	ex 432	. . 3 |- ( ph -> ( x e. ( G tsums F ) -> x e. ( ( cls ` J ) ` { X } ) ) )
79	78	ssrdv 3440	. 2 |- ( ph -> ( G tsums F ) C_ ( ( cls ` J ) ` { X } ) )
80	11, 8, 15, 17, 18, 19, 22	tsmscls 20744	. 2 |- ( ph -> ( ( cls ` J ) ` { X } ) C_ ( G tsums F ) )
81	79, 80	eqssd 3451	1 |- ( ph -> ( G tsums F ) = ( ( cls ` J ) ` { X } ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   /\ w3a 971   = wceq 1399   e. wcel 1836   _Vcvv 3051   C_ wss 3406   {csn 3961   class class class wbr 4384   |-> cmpt 4442   X. cxp 4928   Rel wrel 4935   -->wf 5509   ` cfv 5513  (class class class)co 6218   oFcof 6459   Er wer 7248   [cec 7249   finSupp cfsupp 7766   Basecbs 14657   TopOpenctopn 14852   0gc0g 14870   gsum_g cgsu 14871   Mndcmnd 16059   Grpcgrp 16193   -gcsg 16195  SubGrpcsubg 16335   ~_QG cqg 16337  CMndccmn 16938   Abelcabl 16939   TopSpctps 19505   clsccl 19627   TopGrpctgp 20678   tsums ctsu 20732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-rep 4495  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-cnex 9481  ax-resscn 9482  ax-1cn 9483  ax-icn 9484  ax-addcl 9485  ax-addrcl 9486  ax-mulcl 9487  ax-mulrcl 9488  ax-mulcom 9489  ax-addass 9490  ax-mulass 9491  ax-distr 9492  ax-i2m1 9493  ax-1ne0 9494  ax-1rid 9495  ax-rnegex 9496  ax-rrecex 9497  ax-cnre 9498  ax-pre-lttri 9499  ax-pre-lttrn 9500  ax-pre-ltadd 9501  ax-pre-mulgt0 9502

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-nel 2594  df-ral 2751  df-rex 2752  df-reu 2753  df-rmo 2754  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4181  df-int 4217  df-iun 4262  df-iin 4263  df-br 4385  df-opab 4443  df-mpt 4444  df-tr 4478  df-eprel 4722  df-id 4726  df-po 4731  df-so 4732  df-fr 4769  df-se 4770  df-we 4771  df-ord 4812  df-on 4813  df-lim 4814  df-suc 4815  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-isom 5522  df-riota 6180  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-of 6461  df-om 6622  df-1st 6721  df-2nd 6722  df-supp 6840  df-recs 6982  df-rdg 7016  df-1o 7070  df-oadd 7074  df-er 7251  df-ec 7253  df-map 7362  df-en 7458  df-dom 7459  df-sdom 7460  df-fin 7461  df-fsupp 7767  df-oi 7872  df-card 8255  df-pnf 9563  df-mnf 9564  df-xr 9565  df-ltxr 9566  df-le 9567  df-sub 9742  df-neg 9743  df-nn 10475  df-2 10533  df-n0 10735  df-z 10804  df-uz 11024  df-fz 11616  df-fzo 11740  df-seq 12034  df-hash 12331  df-ndx 14660  df-slot 14661  df-base 14662  df-sets 14663  df-ress 14664  df-plusg 14738  df-0g 14872  df-gsum 14873  df-topgen 14874  df-plusf 16011  df-mgm 16012  df-sgrp 16051  df-mnd 16061  df-mhm 16106  df-submnd 16107  df-grp 16197  df-minusg 16198  df-sbg 16199  df-subg 16338  df-eqg 16340  df-ghm 16405  df-cntz 16495  df-cmn 16940  df-abl 16941  df-fbas 18552  df-fg 18553  df-top 19507  df-bases 19509  df-topon 19510  df-topsp 19511  df-cld 19628  df-ntr 19629  df-cls 19630  df-nei 19708  df-cn 19837  df-cnp 19838  df-tx 20171  df-hmeo 20364  df-fil 20455  df-fm 20547  df-flim 20548  df-flf 20549  df-tmd 20679  df-tgp 20680  df-tsms 20733

This theorem is referenced by:  tgptsmscld  20761