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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
tgptsmscls.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
tgptsmscls.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tgptsmscls.2 ⊢ ( 𝜑 → 𝐺 ∈ TopGrp )
tgptsmscls.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tgptsmscls.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
tgptsmscls.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
Assertion tgptsmscls ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( cls ‘ 𝐽 ) ‘ { 𝑋 } ) )

Proof

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