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 = ( 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 tgptsmscls 
|- ( ph -> ( G tsums F ) = ( ( cls ` J ) ` { X } ) )

Proof

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