Step | Hyp | Ref
| Expression |
1 | | tgptsmscls.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ TopGrp) |
2 | 1 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ TopGrp) |
3 | | tgpgrp 22975 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ Grp) |
5 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘𝐺) = (0g‘𝐺) |
6 | 5 | 0subg 18568 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp →
{(0g‘𝐺)}
∈ (SubGrp‘𝐺)) |
7 | 4, 6 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → {(0g‘𝐺)} ∈ (SubGrp‘𝐺)) |
8 | | tgptsmscls.j |
. . . . . . . . . 10
⊢ 𝐽 = (TopOpen‘𝐺) |
9 | 8 | clssubg 23006 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧
{(0g‘𝐺)}
∈ (SubGrp‘𝐺))
→ ((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺)) |
10 | 2, 7, 9 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → ((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺)) |
11 | | tgptsmscls.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
12 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝐺 ~QG
((cls‘𝐽)‘{(0g‘𝐺)})) = (𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) |
13 | 11, 12 | eqger 18594 |
. . . . . . . 8
⊢
(((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺) → (𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) Er 𝐵) |
14 | 10, 13 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) Er 𝐵) |
15 | | tgptsmscls.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ CMnd) |
16 | | tgptps 22977 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp) |
17 | 1, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ TopSp) |
18 | | tgptsmscls.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
19 | | tgptsmscls.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
20 | 11, 15, 17, 18, 19 | tsmscl 23032 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ 𝐵) |
21 | 20 | sselda 3901 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ 𝐵) |
22 | | tgptsmscls.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) |
23 | 20, 22 | sseldd 3902 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
24 | 23 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑋 ∈ 𝐵) |
25 | | eqid 2737 |
. . . . . . . . . 10
⊢
(-g‘𝐺) = (-g‘𝐺) |
26 | 15 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ CMnd) |
27 | 18 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐴 ∈ 𝑉) |
28 | 19 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐹:𝐴⟶𝐵) |
29 | 22 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑋 ∈ (𝐺 tsums 𝐹)) |
30 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ (𝐺 tsums 𝐹)) |
31 | 11, 25, 26, 2, 27, 28, 28, 29, 30 | tsmssub 23046 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑋(-g‘𝐺)𝑥) ∈ (𝐺 tsums (𝐹 ∘f
(-g‘𝐺)𝐹))) |
32 | 28 | ffvelrnda 6904 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝐵) |
33 | 28 | feqmptd 6780 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
34 | 27, 32, 32, 33, 33 | offval2 7488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐹 ∘f
(-g‘𝐺)𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘)))) |
35 | 4 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → 𝐺 ∈ Grp) |
36 | 11, 5, 25 | grpsubid 18447 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ (𝐹‘𝑘) ∈ 𝐵) → ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘)) = (0g‘𝐺)) |
37 | 35, 32, 36 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘)) = (0g‘𝐺)) |
38 | 37 | mpteq2dva 5150 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘))) = (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) |
39 | 34, 38 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐹 ∘f
(-g‘𝐺)𝐹) = (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) |
40 | 39 | oveq2d 7229 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 tsums (𝐹 ∘f
(-g‘𝐺)𝐹)) = (𝐺 tsums (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))) |
41 | 2, 16 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ TopSp) |
42 | 11, 5 | grpidcl 18395 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐵) |
43 | 4, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (0g‘𝐺) ∈ 𝐵) |
44 | 43 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → (0g‘𝐺) ∈ 𝐵) |
45 | 44 | fmpttd 6932 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)):𝐴⟶𝐵) |
46 | | fconstmpt 5611 |
. . . . . . . . . . . 12
⊢ (𝐴 ×
{(0g‘𝐺)})
= (𝑘 ∈ 𝐴 ↦
(0g‘𝐺)) |
47 | | fvexd 6732 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐺) ∈ V) |
48 | 18, 47 | fczfsuppd 9003 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 × {(0g‘𝐺)}) finSupp
(0g‘𝐺)) |
49 | 48 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐴 × {(0g‘𝐺)}) finSupp
(0g‘𝐺)) |
50 | 46, 49 | eqbrtrrid 5089 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)) finSupp
(0g‘𝐺)) |
51 | 11, 5, 26, 41, 27, 45, 50, 8 | tsmsgsum 23036 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 tsums (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) = ((cls‘𝐽)‘{(𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))})) |
52 | | cmnmnd 19186 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
53 | 26, 52 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ Mnd) |
54 | 5 | gsumz 18262 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) = (0g‘𝐺)) |
55 | 53, 27, 54 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) = (0g‘𝐺)) |
56 | 55 | sneqd 4553 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → {(𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))} =
{(0g‘𝐺)}) |
57 | 56 | fveq2d 6721 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → ((cls‘𝐽)‘{(𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))}) = ((cls‘𝐽)‘{(0g‘𝐺)})) |
58 | 40, 51, 57 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 tsums (𝐹 ∘f
(-g‘𝐺)𝐹)) = ((cls‘𝐽)‘{(0g‘𝐺)})) |
59 | 31, 58 | eleqtrd 2840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑋(-g‘𝐺)𝑥) ∈ ((cls‘𝐽)‘{(0g‘𝐺)})) |
60 | | isabl 19174 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
61 | 4, 26, 60 | sylanbrc 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ Abel) |
62 | 11 | subgss 18544 |
. . . . . . . . . 10
⊢
(((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺) → ((cls‘𝐽)‘{(0g‘𝐺)}) ⊆ 𝐵) |
63 | 10, 62 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → ((cls‘𝐽)‘{(0g‘𝐺)}) ⊆ 𝐵) |
64 | 11, 25, 12 | eqgabl 19220 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Abel ∧
((cls‘𝐽)‘{(0g‘𝐺)}) ⊆ 𝐵) → (𝑥(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑋 ↔ (𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑋(-g‘𝐺)𝑥) ∈ ((cls‘𝐽)‘{(0g‘𝐺)})))) |
65 | 61, 63, 64 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑥(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑋 ↔ (𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑋(-g‘𝐺)𝑥) ∈ ((cls‘𝐽)‘{(0g‘𝐺)})))) |
66 | 21, 24, 59, 65 | mpbir3and 1344 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑋) |
67 | 14, 66 | ersym 8403 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑋(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑥) |
68 | 12 | releqg 18591 |
. . . . . . 7
⊢ Rel
(𝐺 ~QG
((cls‘𝐽)‘{(0g‘𝐺)})) |
69 | | relelec 8436 |
. . . . . . 7
⊢ (Rel
(𝐺 ~QG
((cls‘𝐽)‘{(0g‘𝐺)})) → (𝑥 ∈ [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) ↔ 𝑋(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑥)) |
70 | 68, 69 | ax-mp 5 |
. . . . . 6
⊢ (𝑥 ∈ [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) ↔ 𝑋(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑥) |
71 | 67, 70 | sylibr 237 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))) |
72 | | eqid 2737 |
. . . . . . 7
⊢
((cls‘𝐽)‘{(0g‘𝐺)}) = ((cls‘𝐽)‘{(0g‘𝐺)}) |
73 | 11, 8, 5, 12, 72 | snclseqg 23013 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑋 ∈ 𝐵) → [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) = ((cls‘𝐽)‘{𝑋})) |
74 | 2, 24, 73 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) = ((cls‘𝐽)‘{𝑋})) |
75 | 71, 74 | eleqtrd 2840 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ ((cls‘𝐽)‘{𝑋})) |
76 | 75 | ex 416 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) → 𝑥 ∈ ((cls‘𝐽)‘{𝑋}))) |
77 | 76 | ssrdv 3907 |
. 2
⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ ((cls‘𝐽)‘{𝑋})) |
78 | 11, 8, 15, 17, 18, 19, 22 | tsmscls 23035 |
. 2
⊢ (𝜑 → ((cls‘𝐽)‘{𝑋}) ⊆ (𝐺 tsums 𝐹)) |
79 | 77, 78 | eqssd 3918 |
1
⊢ (𝜑 → (𝐺 tsums 𝐹) = ((cls‘𝐽)‘{𝑋})) |