Step | Hyp | Ref
| Expression |
1 | | tgptsmscls.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ TopGrp) |
2 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ TopGrp) |
3 | | tgpgrp 21692 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ Grp) |
5 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(0g‘𝐺) = (0g‘𝐺) |
6 | 5 | 0subg 17442 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp →
{(0g‘𝐺)}
∈ (SubGrp‘𝐺)) |
7 | 4, 6 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → {(0g‘𝐺)} ∈ (SubGrp‘𝐺)) |
8 | | tgptsmscls.j |
. . . . . . . . . 10
⊢ 𝐽 = (TopOpen‘𝐺) |
9 | 8 | clssubg 21722 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧
{(0g‘𝐺)}
∈ (SubGrp‘𝐺))
→ ((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺)) |
10 | 2, 7, 9 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → ((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺)) |
11 | | tgptsmscls.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
12 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝐺 ~QG
((cls‘𝐽)‘{(0g‘𝐺)})) = (𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) |
13 | 11, 12 | eqger 17467 |
. . . . . . . 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 21694 |
. . . . . . . . . . 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 21748 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ 𝐵) |
21 | 20 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ 𝐵) |
22 | | tgptsmscls.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) |
23 | 20, 22 | sseldd 3569 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
24 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑋 ∈ 𝐵) |
25 | | eqid 2610 |
. . . . . . . . . 10
⊢
(-g‘𝐺) = (-g‘𝐺) |
26 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ CMnd) |
27 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐴 ∈ 𝑉) |
28 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐹:𝐴⟶𝐵) |
29 | 22 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑋 ∈ (𝐺 tsums 𝐹)) |
30 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ (𝐺 tsums 𝐹)) |
31 | 11, 25, 26, 2, 27, 28, 28, 29, 30 | tsmssub 21762 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑋(-g‘𝐺)𝑥) ∈ (𝐺 tsums (𝐹 ∘𝑓
(-g‘𝐺)𝐹))) |
32 | 28 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝐵) |
33 | 28 | feqmptd 6159 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
34 | 27, 32, 32, 33, 33 | offval2 6812 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐹 ∘𝑓
(-g‘𝐺)𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘)))) |
35 | 4 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → 𝐺 ∈ Grp) |
36 | 11, 5, 25 | grpsubid 17322 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ (𝐹‘𝑘) ∈ 𝐵) → ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘)) = (0g‘𝐺)) |
37 | 35, 32, 36 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘)) = (0g‘𝐺)) |
38 | 37 | mpteq2dva 4672 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘))) = (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) |
39 | 34, 38 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐹 ∘𝑓
(-g‘𝐺)𝐹) = (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) |
40 | 39 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 tsums (𝐹 ∘𝑓
(-g‘𝐺)𝐹)) = (𝐺 tsums (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))) |
41 | 2, 16 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ TopSp) |
42 | 11, 5 | grpidcl 17273 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐵) |
43 | 4, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (0g‘𝐺) ∈ 𝐵) |
44 | 43 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → (0g‘𝐺) ∈ 𝐵) |
45 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)) = (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)) |
46 | 44, 45 | fmptd 6292 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)):𝐴⟶𝐵) |
47 | | fconstmpt 5085 |
. . . . . . . . . . . 12
⊢ (𝐴 ×
{(0g‘𝐺)})
= (𝑘 ∈ 𝐴 ↦
(0g‘𝐺)) |
48 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐺) ∈ V |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐺) ∈ V) |
50 | 18, 49 | fczfsuppd 8176 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 × {(0g‘𝐺)}) finSupp
(0g‘𝐺)) |
51 | 50 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐴 × {(0g‘𝐺)}) finSupp
(0g‘𝐺)) |
52 | 47, 51 | syl5eqbrr 4619 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)) finSupp
(0g‘𝐺)) |
53 | 11, 5, 26, 41, 27, 46, 52, 8 | tsmsgsum 21752 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 tsums (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) = ((cls‘𝐽)‘{(𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))})) |
54 | | cmnmnd 18031 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
55 | 26, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ Mnd) |
56 | 5 | gsumz 17197 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) = (0g‘𝐺)) |
57 | 55, 27, 56 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) = (0g‘𝐺)) |
58 | 57 | sneqd 4137 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → {(𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))} =
{(0g‘𝐺)}) |
59 | 58 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → ((cls‘𝐽)‘{(𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))}) = ((cls‘𝐽)‘{(0g‘𝐺)})) |
60 | 40, 53, 59 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 tsums (𝐹 ∘𝑓
(-g‘𝐺)𝐹)) = ((cls‘𝐽)‘{(0g‘𝐺)})) |
61 | 31, 60 | eleqtrd 2690 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑋(-g‘𝐺)𝑥) ∈ ((cls‘𝐽)‘{(0g‘𝐺)})) |
62 | | isabl 18020 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
63 | 4, 26, 62 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ Abel) |
64 | 11 | subgss 17418 |
. . . . . . . . . 10
⊢
(((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺) → ((cls‘𝐽)‘{(0g‘𝐺)}) ⊆ 𝐵) |
65 | 10, 64 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → ((cls‘𝐽)‘{(0g‘𝐺)}) ⊆ 𝐵) |
66 | 11, 25, 12 | eqgabl 18063 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Abel ∧
((cls‘𝐽)‘{(0g‘𝐺)}) ⊆ 𝐵) → (𝑥(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑋 ↔ (𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑋(-g‘𝐺)𝑥) ∈ ((cls‘𝐽)‘{(0g‘𝐺)})))) |
67 | 63, 65, 66 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑥(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑋 ↔ (𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑋(-g‘𝐺)𝑥) ∈ ((cls‘𝐽)‘{(0g‘𝐺)})))) |
68 | 21, 24, 61, 67 | mpbir3and 1238 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑋) |
69 | 14, 68 | ersym 7641 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑋(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑥) |
70 | 12 | releqg 17464 |
. . . . . . 7
⊢ Rel
(𝐺 ~QG
((cls‘𝐽)‘{(0g‘𝐺)})) |
71 | | relelec 7674 |
. . . . . . 7
⊢ (Rel
(𝐺 ~QG
((cls‘𝐽)‘{(0g‘𝐺)})) → (𝑥 ∈ [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) ↔ 𝑋(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑥)) |
72 | 70, 71 | ax-mp 5 |
. . . . . 6
⊢ (𝑥 ∈ [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) ↔ 𝑋(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑥) |
73 | 69, 72 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))) |
74 | | eqid 2610 |
. . . . . . 7
⊢
((cls‘𝐽)‘{(0g‘𝐺)}) = ((cls‘𝐽)‘{(0g‘𝐺)}) |
75 | 11, 8, 5, 12, 74 | snclseqg 21729 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑋 ∈ 𝐵) → [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) = ((cls‘𝐽)‘{𝑋})) |
76 | 2, 24, 75 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) = ((cls‘𝐽)‘{𝑋})) |
77 | 73, 76 | eleqtrd 2690 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ ((cls‘𝐽)‘{𝑋})) |
78 | 77 | ex 449 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) → 𝑥 ∈ ((cls‘𝐽)‘{𝑋}))) |
79 | 78 | ssrdv 3574 |
. 2
⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ ((cls‘𝐽)‘{𝑋})) |
80 | 11, 8, 15, 17, 18, 19, 22 | tsmscls 21751 |
. 2
⊢ (𝜑 → ((cls‘𝐽)‘{𝑋}) ⊆ (𝐺 tsums 𝐹)) |
81 | 79, 80 | eqssd 3585 |
1
⊢ (𝜑 → (𝐺 tsums 𝐹) = ((cls‘𝐽)‘{𝑋})) |