Step | Hyp | Ref
| Expression |
1 | | tgptsmscls.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ TopGrp) |
2 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ TopGrp) |
3 | | tgpgrp 21882 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ Grp) |
5 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(0g‘𝐺) = (0g‘𝐺) |
6 | 5 | 0subg 17619 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp →
{(0g‘𝐺)}
∈ (SubGrp‘𝐺)) |
7 | 4, 6 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → {(0g‘𝐺)} ∈ (SubGrp‘𝐺)) |
8 | | tgptsmscls.j |
. . . . . . . . . 10
⊢ 𝐽 = (TopOpen‘𝐺) |
9 | 8 | clssubg 21912 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧
{(0g‘𝐺)}
∈ (SubGrp‘𝐺))
→ ((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺)) |
10 | 2, 7, 9 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → ((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺)) |
11 | | tgptsmscls.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
12 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝐺 ~QG
((cls‘𝐽)‘{(0g‘𝐺)})) = (𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) |
13 | 11, 12 | eqger 17644 |
. . . . . . . 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 21884 |
. . . . . . . . . . 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 21938 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ 𝐵) |
21 | 20 | sselda 3603 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ 𝐵) |
22 | | tgptsmscls.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) |
23 | 20, 22 | sseldd 3604 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
24 | 23 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑋 ∈ 𝐵) |
25 | | eqid 2622 |
. . . . . . . . . 10
⊢
(-g‘𝐺) = (-g‘𝐺) |
26 | 15 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ CMnd) |
27 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐴 ∈ 𝑉) |
28 | 19 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐹:𝐴⟶𝐵) |
29 | 22 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑋 ∈ (𝐺 tsums 𝐹)) |
30 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ (𝐺 tsums 𝐹)) |
31 | 11, 25, 26, 2, 27, 28, 28, 29, 30 | tsmssub 21952 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑋(-g‘𝐺)𝑥) ∈ (𝐺 tsums (𝐹 ∘𝑓
(-g‘𝐺)𝐹))) |
32 | 28 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝐵) |
33 | 28 | feqmptd 6249 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
34 | 27, 32, 32, 33, 33 | offval2 6914 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐹 ∘𝑓
(-g‘𝐺)𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘)))) |
35 | 4 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → 𝐺 ∈ Grp) |
36 | 11, 5, 25 | grpsubid 17499 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ (𝐹‘𝑘) ∈ 𝐵) → ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘)) = (0g‘𝐺)) |
37 | 35, 32, 36 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘)) = (0g‘𝐺)) |
38 | 37 | mpteq2dva 4744 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘))) = (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) |
39 | 34, 38 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐹 ∘𝑓
(-g‘𝐺)𝐹) = (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) |
40 | 39 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 tsums (𝐹 ∘𝑓
(-g‘𝐺)𝐹)) = (𝐺 tsums (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))) |
41 | 2, 16 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ TopSp) |
42 | 11, 5 | grpidcl 17450 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐵) |
43 | 4, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (0g‘𝐺) ∈ 𝐵) |
44 | 43 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → (0g‘𝐺) ∈ 𝐵) |
45 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)) = (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)) |
46 | 44, 45 | fmptd 6385 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)):𝐴⟶𝐵) |
47 | | fconstmpt 5163 |
. . . . . . . . . . . 12
⊢ (𝐴 ×
{(0g‘𝐺)})
= (𝑘 ∈ 𝐴 ↦
(0g‘𝐺)) |
48 | | fvexd 6203 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐺) ∈ V) |
49 | 18, 48 | fczfsuppd 8293 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 × {(0g‘𝐺)}) finSupp
(0g‘𝐺)) |
50 | 49 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐴 × {(0g‘𝐺)}) finSupp
(0g‘𝐺)) |
51 | 47, 50 | syl5eqbrr 4689 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)) finSupp
(0g‘𝐺)) |
52 | 11, 5, 26, 41, 27, 46, 51, 8 | tsmsgsum 21942 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 tsums (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) = ((cls‘𝐽)‘{(𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))})) |
53 | | cmnmnd 18208 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
54 | 26, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ Mnd) |
55 | 5 | gsumz 17374 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) = (0g‘𝐺)) |
56 | 54, 27, 55 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) = (0g‘𝐺)) |
57 | 56 | sneqd 4189 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → {(𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))} =
{(0g‘𝐺)}) |
58 | 57 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → ((cls‘𝐽)‘{(𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))}) = ((cls‘𝐽)‘{(0g‘𝐺)})) |
59 | 40, 52, 58 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 tsums (𝐹 ∘𝑓
(-g‘𝐺)𝐹)) = ((cls‘𝐽)‘{(0g‘𝐺)})) |
60 | 31, 59 | eleqtrd 2703 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑋(-g‘𝐺)𝑥) ∈ ((cls‘𝐽)‘{(0g‘𝐺)})) |
61 | | isabl 18197 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
62 | 4, 26, 61 | sylanbrc 698 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ Abel) |
63 | 11 | subgss 17595 |
. . . . . . . . . 10
⊢
(((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺) → ((cls‘𝐽)‘{(0g‘𝐺)}) ⊆ 𝐵) |
64 | 10, 63 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → ((cls‘𝐽)‘{(0g‘𝐺)}) ⊆ 𝐵) |
65 | 11, 25, 12 | eqgabl 18240 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Abel ∧
((cls‘𝐽)‘{(0g‘𝐺)}) ⊆ 𝐵) → (𝑥(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑋 ↔ (𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑋(-g‘𝐺)𝑥) ∈ ((cls‘𝐽)‘{(0g‘𝐺)})))) |
66 | 62, 64, 65 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑥(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑋 ↔ (𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑋(-g‘𝐺)𝑥) ∈ ((cls‘𝐽)‘{(0g‘𝐺)})))) |
67 | 21, 24, 60, 66 | mpbir3and 1245 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑋) |
68 | 14, 67 | ersym 7754 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑋(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑥) |
69 | 12 | releqg 17641 |
. . . . . . 7
⊢ Rel
(𝐺 ~QG
((cls‘𝐽)‘{(0g‘𝐺)})) |
70 | | relelec 7787 |
. . . . . . 7
⊢ (Rel
(𝐺 ~QG
((cls‘𝐽)‘{(0g‘𝐺)})) → (𝑥 ∈ [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) ↔ 𝑋(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑥)) |
71 | 69, 70 | ax-mp 5 |
. . . . . 6
⊢ (𝑥 ∈ [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) ↔ 𝑋(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑥) |
72 | 68, 71 | sylibr 224 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))) |
73 | | eqid 2622 |
. . . . . . 7
⊢
((cls‘𝐽)‘{(0g‘𝐺)}) = ((cls‘𝐽)‘{(0g‘𝐺)}) |
74 | 11, 8, 5, 12, 73 | snclseqg 21919 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑋 ∈ 𝐵) → [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) = ((cls‘𝐽)‘{𝑋})) |
75 | 2, 24, 74 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) = ((cls‘𝐽)‘{𝑋})) |
76 | 72, 75 | eleqtrd 2703 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ ((cls‘𝐽)‘{𝑋})) |
77 | 76 | ex 450 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) → 𝑥 ∈ ((cls‘𝐽)‘{𝑋}))) |
78 | 77 | ssrdv 3609 |
. 2
⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ ((cls‘𝐽)‘{𝑋})) |
79 | 11, 8, 15, 17, 18, 19, 22 | tsmscls 21941 |
. 2
⊢ (𝜑 → ((cls‘𝐽)‘{𝑋}) ⊆ (𝐺 tsums 𝐹)) |
80 | 78, 79 | eqssd 3620 |
1
⊢ (𝜑 → (𝐺 tsums 𝐹) = ((cls‘𝐽)‘{𝑋})) |