| Step | Hyp | Ref
| Expression |
| 1 | | tgptsmscls.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ TopGrp) |
| 2 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ TopGrp) |
| 3 | | tgpgrp 24086 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
| 4 | 2, 3 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ Grp) |
| 5 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 6 | 5 | 0subg 19169 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp →
{(0g‘𝐺)}
∈ (SubGrp‘𝐺)) |
| 7 | 4, 6 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → {(0g‘𝐺)} ∈ (SubGrp‘𝐺)) |
| 8 | | tgptsmscls.j |
. . . . . . . . . 10
⊢ 𝐽 = (TopOpen‘𝐺) |
| 9 | 8 | clssubg 24117 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧
{(0g‘𝐺)}
∈ (SubGrp‘𝐺))
→ ((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺)) |
| 10 | 2, 7, 9 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → ((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺)) |
| 11 | | tgptsmscls.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
| 12 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝐺 ~QG
((cls‘𝐽)‘{(0g‘𝐺)})) = (𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) |
| 13 | 11, 12 | eqger 19196 |
. . . . . . . 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 24088 |
. . . . . . . . . . 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 24143 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ 𝐵) |
| 21 | 20 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ 𝐵) |
| 22 | | tgptsmscls.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) |
| 23 | 20, 22 | sseldd 3984 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 24 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑋 ∈ 𝐵) |
| 25 | | eqid 2737 |
. . . . . . . . . 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 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ (𝐺 tsums 𝐹)) |
| 31 | 11, 25, 26, 2, 27, 28, 28, 29, 30 | tsmssub 24157 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑋(-g‘𝐺)𝑥) ∈ (𝐺 tsums (𝐹 ∘f
(-g‘𝐺)𝐹))) |
| 32 | 28 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝐵) |
| 33 | 28 | feqmptd 6977 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
| 34 | 27, 32, 32, 33, 33 | offval2 7717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐹 ∘f
(-g‘𝐺)𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘)))) |
| 35 | 4 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → 𝐺 ∈ Grp) |
| 36 | 11, 5, 25 | grpsubid 19042 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ (𝐹‘𝑘) ∈ 𝐵) → ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘)) = (0g‘𝐺)) |
| 37 | 35, 32, 36 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘)) = (0g‘𝐺)) |
| 38 | 37 | mpteq2dva 5242 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)(-g‘𝐺)(𝐹‘𝑘))) = (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) |
| 39 | 34, 38 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐹 ∘f
(-g‘𝐺)𝐹) = (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) |
| 40 | 39 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 tsums (𝐹 ∘f
(-g‘𝐺)𝐹)) = (𝐺 tsums (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))) |
| 41 | 2, 16 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ TopSp) |
| 42 | 11, 5 | grpidcl 18983 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐵) |
| 43 | 4, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (0g‘𝐺) ∈ 𝐵) |
| 44 | 43 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ∧ 𝑘 ∈ 𝐴) → (0g‘𝐺) ∈ 𝐵) |
| 45 | 44 | fmpttd 7135 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)):𝐴⟶𝐵) |
| 46 | | fconstmpt 5747 |
. . . . . . . . . . . 12
⊢ (𝐴 ×
{(0g‘𝐺)})
= (𝑘 ∈ 𝐴 ↦
(0g‘𝐺)) |
| 47 | | fvexd 6921 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐺) ∈ V) |
| 48 | 18, 47 | fczfsuppd 9426 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 × {(0g‘𝐺)}) finSupp
(0g‘𝐺)) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐴 × {(0g‘𝐺)}) finSupp
(0g‘𝐺)) |
| 50 | 46, 49 | eqbrtrrid 5179 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)) finSupp
(0g‘𝐺)) |
| 51 | 11, 5, 26, 41, 27, 45, 50, 8 | tsmsgsum 24147 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 tsums (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) = ((cls‘𝐽)‘{(𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))})) |
| 52 | | cmnmnd 19815 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
| 53 | 26, 52 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ Mnd) |
| 54 | 5 | gsumz 18849 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) = (0g‘𝐺)) |
| 55 | 53, 27, 54 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺))) = (0g‘𝐺)) |
| 56 | 55 | sneqd 4638 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → {(𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))} =
{(0g‘𝐺)}) |
| 57 | 56 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → ((cls‘𝐽)‘{(𝐺 Σg (𝑘 ∈ 𝐴 ↦ (0g‘𝐺)))}) = ((cls‘𝐽)‘{(0g‘𝐺)})) |
| 58 | 40, 51, 57 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝐺 tsums (𝐹 ∘f
(-g‘𝐺)𝐹)) = ((cls‘𝐽)‘{(0g‘𝐺)})) |
| 59 | 31, 58 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑋(-g‘𝐺)𝑥) ∈ ((cls‘𝐽)‘{(0g‘𝐺)})) |
| 60 | | isabl 19802 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
| 61 | 4, 26, 60 | sylanbrc 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝐺 ∈ Abel) |
| 62 | 11 | subgss 19145 |
. . . . . . . . . 10
⊢
(((cls‘𝐽)‘{(0g‘𝐺)}) ∈ (SubGrp‘𝐺) → ((cls‘𝐽)‘{(0g‘𝐺)}) ⊆ 𝐵) |
| 63 | 10, 62 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → ((cls‘𝐽)‘{(0g‘𝐺)}) ⊆ 𝐵) |
| 64 | 11, 25, 12 | eqgabl 19852 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Abel ∧
((cls‘𝐽)‘{(0g‘𝐺)}) ⊆ 𝐵) → (𝑥(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑋 ↔ (𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑋(-g‘𝐺)𝑥) ∈ ((cls‘𝐽)‘{(0g‘𝐺)})))) |
| 65 | 61, 63, 64 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → (𝑥(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑋 ↔ (𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑋(-g‘𝐺)𝑥) ∈ ((cls‘𝐽)‘{(0g‘𝐺)})))) |
| 66 | 21, 24, 59, 65 | mpbir3and 1343 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑋) |
| 67 | 14, 66 | ersym 8757 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑋(𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))𝑥) |
| 68 | 12 | releqg 19193 |
. . . . . . 7
⊢ Rel
(𝐺 ~QG
((cls‘𝐽)‘{(0g‘𝐺)})) |
| 69 | | relelec 8792 |
. . . . . . 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 234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)}))) |
| 72 | | eqid 2737 |
. . . . . . 7
⊢
((cls‘𝐽)‘{(0g‘𝐺)}) = ((cls‘𝐽)‘{(0g‘𝐺)}) |
| 73 | 11, 8, 5, 12, 72 | snclseqg 24124 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑋 ∈ 𝐵) → [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) = ((cls‘𝐽)‘{𝑋})) |
| 74 | 2, 24, 73 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → [𝑋](𝐺 ~QG ((cls‘𝐽)‘{(0g‘𝐺)})) = ((cls‘𝐽)‘{𝑋})) |
| 75 | 71, 74 | eleqtrd 2843 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) → 𝑥 ∈ ((cls‘𝐽)‘{𝑋})) |
| 76 | 75 | ex 412 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) → 𝑥 ∈ ((cls‘𝐽)‘{𝑋}))) |
| 77 | 76 | ssrdv 3989 |
. 2
⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ ((cls‘𝐽)‘{𝑋})) |
| 78 | 11, 8, 15, 17, 18, 19, 22 | tsmscls 24146 |
. 2
⊢ (𝜑 → ((cls‘𝐽)‘{𝑋}) ⊆ (𝐺 tsums 𝐹)) |
| 79 | 77, 78 | eqssd 4001 |
1
⊢ (𝜑 → (𝐺 tsums 𝐹) = ((cls‘𝐽)‘{𝑋})) |