Step | Hyp | Ref
| Expression |
1 | | tgptsmscls.2 |
. . . . . . . . . 10
β’ (π β πΊ β TopGrp) |
2 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β πΊ β TopGrp) |
3 | | tgpgrp 23445 |
. . . . . . . . . . 11
β’ (πΊ β TopGrp β πΊ β Grp) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β πΊ β Grp) |
5 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0gβπΊ) = (0gβπΊ) |
6 | 5 | 0subg 18958 |
. . . . . . . . . 10
β’ (πΊ β Grp β
{(0gβπΊ)}
β (SubGrpβπΊ)) |
7 | 4, 6 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β {(0gβπΊ)} β (SubGrpβπΊ)) |
8 | | tgptsmscls.j |
. . . . . . . . . 10
β’ π½ = (TopOpenβπΊ) |
9 | 8 | clssubg 23476 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§
{(0gβπΊ)}
β (SubGrpβπΊ))
β ((clsβπ½)β{(0gβπΊ)}) β (SubGrpβπΊ)) |
10 | 2, 7, 9 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β ((clsβπ½)β{(0gβπΊ)}) β (SubGrpβπΊ)) |
11 | | tgptsmscls.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΊ) |
12 | | eqid 2733 |
. . . . . . . . 9
β’ (πΊ ~QG
((clsβπ½)β{(0gβπΊ)})) = (πΊ ~QG ((clsβπ½)β{(0gβπΊ)})) |
13 | 11, 12 | eqger 18985 |
. . . . . . . 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 23447 |
. . . . . . . . . . 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 23502 |
. . . . . . . . 9
β’ (π β (πΊ tsums πΉ) β π΅) |
21 | 20 | sselda 3945 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β π₯ β π΅) |
22 | | tgptsmscls.x |
. . . . . . . . . 10
β’ (π β π β (πΊ tsums πΉ)) |
23 | 20, 22 | sseldd 3946 |
. . . . . . . . 9
β’ (π β π β π΅) |
24 | 23 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β π β π΅) |
25 | | eqid 2733 |
. . . . . . . . . 10
β’
(-gβπΊ) = (-gβπΊ) |
26 | 15 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β πΊ β CMnd) |
27 | 18 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β π΄ β π) |
28 | 19 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β πΉ:π΄βΆπ΅) |
29 | 22 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β π β (πΊ tsums πΉ)) |
30 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β π₯ β (πΊ tsums πΉ)) |
31 | 11, 25, 26, 2, 27, 28, 28, 29, 30 | tsmssub 23516 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (π(-gβπΊ)π₯) β (πΊ tsums (πΉ βf
(-gβπΊ)πΉ))) |
32 | 28 | ffvelcdmda 7036 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (πΊ tsums πΉ)) β§ π β π΄) β (πΉβπ) β π΅) |
33 | 28 | feqmptd 6911 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β πΉ = (π β π΄ β¦ (πΉβπ))) |
34 | 27, 32, 32, 33, 33 | offval2 7638 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (πΉ βf
(-gβπΊ)πΉ) = (π β π΄ β¦ ((πΉβπ)(-gβπΊ)(πΉβπ)))) |
35 | 4 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (πΊ tsums πΉ)) β§ π β π΄) β πΊ β Grp) |
36 | 11, 5, 25 | grpsubid 18836 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Grp β§ (πΉβπ) β π΅) β ((πΉβπ)(-gβπΊ)(πΉβπ)) = (0gβπΊ)) |
37 | 35, 32, 36 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (πΊ tsums πΉ)) β§ π β π΄) β ((πΉβπ)(-gβπΊ)(πΉβπ)) = (0gβπΊ)) |
38 | 37 | mpteq2dva 5206 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (π β π΄ β¦ ((πΉβπ)(-gβπΊ)(πΉβπ))) = (π β π΄ β¦ (0gβπΊ))) |
39 | 34, 38 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (πΉ βf
(-gβπΊ)πΉ) = (π β π΄ β¦ (0gβπΊ))) |
40 | 39 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (πΊ tsums (πΉ βf
(-gβπΊ)πΉ)) = (πΊ tsums (π β π΄ β¦ (0gβπΊ)))) |
41 | 2, 16 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β πΊ β TopSp) |
42 | 11, 5 | grpidcl 18783 |
. . . . . . . . . . . . . 14
β’ (πΊ β Grp β
(0gβπΊ)
β π΅) |
43 | 4, 42 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (0gβπΊ) β π΅) |
44 | 43 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (πΊ tsums πΉ)) β§ π β π΄) β (0gβπΊ) β π΅) |
45 | 44 | fmpttd 7064 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (π β π΄ β¦ (0gβπΊ)):π΄βΆπ΅) |
46 | | fconstmpt 5695 |
. . . . . . . . . . . 12
β’ (π΄ Γ
{(0gβπΊ)})
= (π β π΄ β¦
(0gβπΊ)) |
47 | | fvexd 6858 |
. . . . . . . . . . . . . 14
β’ (π β (0gβπΊ) β V) |
48 | 18, 47 | fczfsuppd 9328 |
. . . . . . . . . . . . 13
β’ (π β (π΄ Γ {(0gβπΊ)}) finSupp
(0gβπΊ)) |
49 | 48 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (π΄ Γ {(0gβπΊ)}) finSupp
(0gβπΊ)) |
50 | 46, 49 | eqbrtrrid 5142 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (π β π΄ β¦ (0gβπΊ)) finSupp
(0gβπΊ)) |
51 | 11, 5, 26, 41, 27, 45, 50, 8 | tsmsgsum 23506 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (πΊ tsums (π β π΄ β¦ (0gβπΊ))) = ((clsβπ½)β{(πΊ Ξ£g (π β π΄ β¦ (0gβπΊ)))})) |
52 | | cmnmnd 19584 |
. . . . . . . . . . . . . 14
β’ (πΊ β CMnd β πΊ β Mnd) |
53 | 26, 52 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β πΊ β Mnd) |
54 | 5 | gsumz 18651 |
. . . . . . . . . . . . 13
β’ ((πΊ β Mnd β§ π΄ β π) β (πΊ Ξ£g (π β π΄ β¦ (0gβπΊ))) = (0gβπΊ)) |
55 | 53, 27, 54 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (πΊ Ξ£g (π β π΄ β¦ (0gβπΊ))) = (0gβπΊ)) |
56 | 55 | sneqd 4599 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β {(πΊ Ξ£g (π β π΄ β¦ (0gβπΊ)))} =
{(0gβπΊ)}) |
57 | 56 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β ((clsβπ½)β{(πΊ Ξ£g (π β π΄ β¦ (0gβπΊ)))}) = ((clsβπ½)β{(0gβπΊ)})) |
58 | 40, 51, 57 | 3eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (πΊ tsums (πΉ βf
(-gβπΊ)πΉ)) = ((clsβπ½)β{(0gβπΊ)})) |
59 | 31, 58 | eleqtrd 2836 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (π(-gβπΊ)π₯) β ((clsβπ½)β{(0gβπΊ)})) |
60 | | isabl 19571 |
. . . . . . . . . 10
β’ (πΊ β Abel β (πΊ β Grp β§ πΊ β CMnd)) |
61 | 4, 26, 60 | sylanbrc 584 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β πΊ β Abel) |
62 | 11 | subgss 18934 |
. . . . . . . . . 10
β’
(((clsβπ½)β{(0gβπΊ)}) β (SubGrpβπΊ) β ((clsβπ½)β{(0gβπΊ)}) β π΅) |
63 | 10, 62 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β ((clsβπ½)β{(0gβπΊ)}) β π΅) |
64 | 11, 25, 12 | eqgabl 19618 |
. . . . . . . . 9
β’ ((πΊ β Abel β§
((clsβπ½)β{(0gβπΊ)}) β π΅) β (π₯(πΊ ~QG ((clsβπ½)β{(0gβπΊ)}))π β (π₯ β π΅ β§ π β π΅ β§ (π(-gβπΊ)π₯) β ((clsβπ½)β{(0gβπΊ)})))) |
65 | 61, 63, 64 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β (π₯(πΊ ~QG ((clsβπ½)β{(0gβπΊ)}))π β (π₯ β π΅ β§ π β π΅ β§ (π(-gβπΊ)π₯) β ((clsβπ½)β{(0gβπΊ)})))) |
66 | 21, 24, 59, 65 | mpbir3and 1343 |
. . . . . . 7
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β π₯(πΊ ~QG ((clsβπ½)β{(0gβπΊ)}))π) |
67 | 14, 66 | ersym 8663 |
. . . . . 6
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β π(πΊ ~QG ((clsβπ½)β{(0gβπΊ)}))π₯) |
68 | 12 | releqg 18982 |
. . . . . . 7
β’ Rel
(πΊ ~QG
((clsβπ½)β{(0gβπΊ)})) |
69 | | relelec 8696 |
. . . . . . 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 233 |
. . . . 5
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β π₯ β [π](πΊ ~QG ((clsβπ½)β{(0gβπΊ)}))) |
72 | | eqid 2733 |
. . . . . . 7
β’
((clsβπ½)β{(0gβπΊ)}) = ((clsβπ½)β{(0gβπΊ)}) |
73 | 11, 8, 5, 12, 72 | snclseqg 23483 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π β π΅) β [π](πΊ ~QG ((clsβπ½)β{(0gβπΊ)})) = ((clsβπ½)β{π})) |
74 | 2, 24, 73 | syl2anc 585 |
. . . . 5
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β [π](πΊ ~QG ((clsβπ½)β{(0gβπΊ)})) = ((clsβπ½)β{π})) |
75 | 71, 74 | eleqtrd 2836 |
. . . 4
β’ ((π β§ π₯ β (πΊ tsums πΉ)) β π₯ β ((clsβπ½)β{π})) |
76 | 75 | ex 414 |
. . 3
β’ (π β (π₯ β (πΊ tsums πΉ) β π₯ β ((clsβπ½)β{π}))) |
77 | 76 | ssrdv 3951 |
. 2
β’ (π β (πΊ tsums πΉ) β ((clsβπ½)β{π})) |
78 | 11, 8, 15, 17, 18, 19, 22 | tsmscls 23505 |
. 2
β’ (π β ((clsβπ½)β{π}) β (πΊ tsums πΉ)) |
79 | 77, 78 | eqssd 3962 |
1
β’ (π β (πΊ tsums πΉ) = ((clsβπ½)β{π})) |