Step | Hyp | Ref
| Expression |
1 | | qustgp.h |
. . . . . . . 8
β’ π» = (πΊ /s (πΊ ~QG π)) |
2 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπΊ) = (0gβπΊ) |
3 | 1, 2 | qus0 19068 |
. . . . . . 7
β’ (π β (NrmSGrpβπΊ) β
[(0gβπΊ)](πΊ ~QG π) = (0gβπ»)) |
4 | 3 | 3ad2ant2 1135 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β [(0gβπΊ)](πΊ ~QG π) = (0gβπ»)) |
5 | | tgpgrp 23582 |
. . . . . . . . 9
β’ (πΊ β TopGrp β πΊ β Grp) |
6 | 5 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β πΊ β Grp) |
7 | | eqid 2733 |
. . . . . . . . 9
β’
(BaseβπΊ) =
(BaseβπΊ) |
8 | 7, 2 | grpidcl 18850 |
. . . . . . . 8
β’ (πΊ β Grp β
(0gβπΊ)
β (BaseβπΊ)) |
9 | 6, 8 | syl 17 |
. . . . . . 7
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β (0gβπΊ) β (BaseβπΊ)) |
10 | | ovex 7442 |
. . . . . . . 8
β’ (πΊ ~QG π) β V |
11 | 10 | ecelqsi 8767 |
. . . . . . 7
β’
((0gβπΊ) β (BaseβπΊ) β [(0gβπΊ)](πΊ ~QG π) β ((BaseβπΊ) / (πΊ ~QG π))) |
12 | 9, 11 | syl 17 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β [(0gβπΊ)](πΊ ~QG π) β ((BaseβπΊ) / (πΊ ~QG π))) |
13 | 4, 12 | eqeltrrd 2835 |
. . . . 5
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β (0gβπ») β ((BaseβπΊ) / (πΊ ~QG π))) |
14 | 13 | snssd 4813 |
. . . 4
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β {(0gβπ»)} β ((BaseβπΊ) / (πΊ ~QG π))) |
15 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)) = (π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)) |
16 | 15 | mptpreima 6238 |
. . . . . 6
β’ (β‘(π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)) β {(0gβπ»)}) = {π₯ β (BaseβπΊ) β£ [π₯](πΊ ~QG π) β {(0gβπ»)}} |
17 | | nsgsubg 19038 |
. . . . . . . . . . 11
β’ (π β (NrmSGrpβπΊ) β π β (SubGrpβπΊ)) |
18 | 17 | 3ad2ant2 1135 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β π β (SubGrpβπΊ)) |
19 | | eqid 2733 |
. . . . . . . . . . 11
β’ (πΊ ~QG π) = (πΊ ~QG π) |
20 | 7, 19, 2 | eqgid 19060 |
. . . . . . . . . 10
β’ (π β (SubGrpβπΊ) β
[(0gβπΊ)](πΊ ~QG π) = π) |
21 | 18, 20 | syl 17 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β [(0gβπΊ)](πΊ ~QG π) = π) |
22 | 7 | subgss 19007 |
. . . . . . . . . 10
β’ (π β (SubGrpβπΊ) β π β (BaseβπΊ)) |
23 | 18, 22 | syl 17 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β π β (BaseβπΊ)) |
24 | 21, 23 | eqsstrd 4021 |
. . . . . . . 8
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β [(0gβπΊ)](πΊ ~QG π) β (BaseβπΊ)) |
25 | | sseqin2 4216 |
. . . . . . . 8
β’
([(0gβπΊ)](πΊ ~QG π) β (BaseβπΊ) β ((BaseβπΊ) β© [(0gβπΊ)](πΊ ~QG π)) = [(0gβπΊ)](πΊ ~QG π)) |
26 | 24, 25 | sylib 217 |
. . . . . . 7
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β ((BaseβπΊ) β© [(0gβπΊ)](πΊ ~QG π)) = [(0gβπΊ)](πΊ ~QG π)) |
27 | 7, 19 | eqger 19058 |
. . . . . . . . . . . . 13
β’ (π β (SubGrpβπΊ) β (πΊ ~QG π) Er (BaseβπΊ)) |
28 | 18, 27 | syl 17 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β (πΊ ~QG π) Er (BaseβπΊ)) |
29 | 28, 9 | erth 8752 |
. . . . . . . . . . 11
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β ((0gβπΊ)(πΊ ~QG π)π₯ β [(0gβπΊ)](πΊ ~QG π) = [π₯](πΊ ~QG π))) |
30 | 29 | adantr 482 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β§ π₯ β (BaseβπΊ)) β ((0gβπΊ)(πΊ ~QG π)π₯ β [(0gβπΊ)](πΊ ~QG π) = [π₯](πΊ ~QG π))) |
31 | 4 | adantr 482 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β§ π₯ β (BaseβπΊ)) β [(0gβπΊ)](πΊ ~QG π) = (0gβπ»)) |
32 | 31 | eqeq1d 2735 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β§ π₯ β (BaseβπΊ)) β ([(0gβπΊ)](πΊ ~QG π) = [π₯](πΊ ~QG π) β (0gβπ») = [π₯](πΊ ~QG π))) |
33 | 30, 32 | bitrd 279 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β§ π₯ β (BaseβπΊ)) β ((0gβπΊ)(πΊ ~QG π)π₯ β (0gβπ») = [π₯](πΊ ~QG π))) |
34 | | vex 3479 |
. . . . . . . . . 10
β’ π₯ β V |
35 | | fvex 6905 |
. . . . . . . . . 10
β’
(0gβπΊ) β V |
36 | 34, 35 | elec 8747 |
. . . . . . . . 9
β’ (π₯ β
[(0gβπΊ)](πΊ ~QG π) β (0gβπΊ)(πΊ ~QG π)π₯) |
37 | | fvex 6905 |
. . . . . . . . . . 11
β’
(0gβπ») β V |
38 | 37 | elsn2 4668 |
. . . . . . . . . 10
β’ ([π₯](πΊ ~QG π) β {(0gβπ»)} β [π₯](πΊ ~QG π) = (0gβπ»)) |
39 | | eqcom 2740 |
. . . . . . . . . 10
β’ ([π₯](πΊ ~QG π) = (0gβπ») β (0gβπ») = [π₯](πΊ ~QG π)) |
40 | 38, 39 | bitri 275 |
. . . . . . . . 9
β’ ([π₯](πΊ ~QG π) β {(0gβπ»)} β
(0gβπ») =
[π₯](πΊ ~QG π)) |
41 | 33, 36, 40 | 3bitr4g 314 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β§ π₯ β (BaseβπΊ)) β (π₯ β [(0gβπΊ)](πΊ ~QG π) β [π₯](πΊ ~QG π) β {(0gβπ»)})) |
42 | 41 | rabbi2dva 4218 |
. . . . . . 7
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β ((BaseβπΊ) β© [(0gβπΊ)](πΊ ~QG π)) = {π₯ β (BaseβπΊ) β£ [π₯](πΊ ~QG π) β {(0gβπ»)}}) |
43 | 26, 42, 21 | 3eqtr3d 2781 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β {π₯ β (BaseβπΊ) β£ [π₯](πΊ ~QG π) β {(0gβπ»)}} = π) |
44 | 16, 43 | eqtrid 2785 |
. . . . 5
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β (β‘(π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)) β {(0gβπ»)}) = π) |
45 | | simp3 1139 |
. . . . 5
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β π β (Clsdβπ½)) |
46 | 44, 45 | eqeltrd 2834 |
. . . 4
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β (β‘(π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)) β {(0gβπ»)}) β (Clsdβπ½)) |
47 | | qustgphaus.j |
. . . . . . 7
β’ π½ = (TopOpenβπΊ) |
48 | 47, 7 | tgptopon 23586 |
. . . . . 6
β’ (πΊ β TopGrp β π½ β
(TopOnβ(BaseβπΊ))) |
49 | 48 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β π½ β (TopOnβ(BaseβπΊ))) |
50 | 1 | a1i 11 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β π» = (πΊ /s (πΊ ~QG π))) |
51 | | eqidd 2734 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β (BaseβπΊ) = (BaseβπΊ)) |
52 | 10 | a1i 11 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β (πΊ ~QG π) β V) |
53 | | simp1 1137 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β πΊ β TopGrp) |
54 | 50, 51, 15, 52, 53 | quslem 17489 |
. . . . 5
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β (π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)):(BaseβπΊ)βontoβ((BaseβπΊ) / (πΊ ~QG π))) |
55 | | qtopcld 23217 |
. . . . 5
β’ ((π½ β
(TopOnβ(BaseβπΊ)) β§ (π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)):(BaseβπΊ)βontoβ((BaseβπΊ) / (πΊ ~QG π))) β ({(0gβπ»)} β (Clsdβ(π½ qTop (π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)))) β ({(0gβπ»)} β ((BaseβπΊ) / (πΊ ~QG π)) β§ (β‘(π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)) β {(0gβπ»)}) β (Clsdβπ½)))) |
56 | 49, 54, 55 | syl2anc 585 |
. . . 4
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β ({(0gβπ»)} β (Clsdβ(π½ qTop (π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)))) β ({(0gβπ»)} β ((BaseβπΊ) / (πΊ ~QG π)) β§ (β‘(π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)) β {(0gβπ»)}) β (Clsdβπ½)))) |
57 | 14, 46, 56 | mpbir2and 712 |
. . 3
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β {(0gβπ»)} β (Clsdβ(π½ qTop (π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π))))) |
58 | 50, 51, 15, 52, 53 | qusval 17488 |
. . . . 5
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β π» = ((π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)) βs πΊ)) |
59 | | qustgphaus.k |
. . . . 5
β’ πΎ = (TopOpenβπ») |
60 | 58, 51, 54, 53, 47, 59 | imastopn 23224 |
. . . 4
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β πΎ = (π½ qTop (π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π)))) |
61 | 60 | fveq2d 6896 |
. . 3
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β (ClsdβπΎ) = (Clsdβ(π½ qTop (π₯ β (BaseβπΊ) β¦ [π₯](πΊ ~QG π))))) |
62 | 57, 61 | eleqtrrd 2837 |
. 2
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β {(0gβπ»)} β (ClsdβπΎ)) |
63 | 1 | qustgp 23626 |
. . . 4
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β π» β TopGrp) |
64 | 63 | 3adant3 1133 |
. . 3
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β π» β TopGrp) |
65 | | eqid 2733 |
. . . 4
β’
(0gβπ») = (0gβπ») |
66 | 65, 59 | tgphaus 23621 |
. . 3
β’ (π» β TopGrp β (πΎ β Haus β
{(0gβπ»)}
β (ClsdβπΎ))) |
67 | 64, 66 | syl 17 |
. 2
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β (πΎ β Haus β
{(0gβπ»)}
β (ClsdβπΎ))) |
68 | 62, 67 | mpbird 257 |
1
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β πΎ β Haus) |