Step | Hyp | Ref
| Expression |
1 | | tngbas.t |
. . 3
β’ π = (πΊ toNrmGrp π) |
2 | | tngtset.2 |
. . 3
β’ π· = (distβπ) |
3 | | tngtset.3 |
. . 3
β’ π½ = (MetOpenβπ·) |
4 | 1, 2, 3 | tngtset 24036 |
. 2
β’ ((πΊ β π β§ π β π) β π½ = (TopSetβπ)) |
5 | | df-mopn 20815 |
. . . . . . . . 9
β’ MetOpen =
(π₯ β βͺ ran βMet β¦ (topGenβran
(ballβπ₯))) |
6 | 5 | dmmptss 6197 |
. . . . . . . 8
β’ dom
MetOpen β βͺ ran βMet |
7 | 6 | sseli 3944 |
. . . . . . 7
β’ (π· β dom MetOpen β π· β βͺ ran βMet) |
8 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(-gβπΊ) = (-gβπΊ) |
9 | 1, 8 | tngds 24034 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (π β (-gβπΊ)) = (distβπ)) |
10 | 9, 2 | eqtr4di 2791 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (π β (-gβπΊ)) = π·) |
11 | 10 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β π β§ π β π) β (π β (-gβπΊ)) = π·) |
12 | 11 | dmeqd 5865 |
. . . . . . . . . . . . . 14
β’ ((πΊ β π β§ π β π) β dom (π β (-gβπΊ)) = dom π·) |
13 | | dmcoss 5930 |
. . . . . . . . . . . . . . 15
β’ dom
(π β
(-gβπΊ))
β dom (-gβπΊ) |
14 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(BaseβπΊ) =
(BaseβπΊ) |
15 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(+gβπΊ) = (+gβπΊ) |
16 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(invgβπΊ) = (invgβπΊ) |
17 | 14, 15, 16, 8 | grpsubfval 18802 |
. . . . . . . . . . . . . . . 16
β’
(-gβπΊ) = (π₯ β (BaseβπΊ), π¦ β (BaseβπΊ) β¦ (π₯(+gβπΊ)((invgβπΊ)βπ¦))) |
18 | | ovex 7394 |
. . . . . . . . . . . . . . . 16
β’ (π₯(+gβπΊ)((invgβπΊ)βπ¦)) β V |
19 | 17, 18 | dmmpo 8007 |
. . . . . . . . . . . . . . 15
β’ dom
(-gβπΊ) =
((BaseβπΊ) Γ
(BaseβπΊ)) |
20 | 13, 19 | sseqtri 3984 |
. . . . . . . . . . . . . 14
β’ dom
(π β
(-gβπΊ))
β ((BaseβπΊ)
Γ (BaseβπΊ)) |
21 | 12, 20 | eqsstrrdi 4003 |
. . . . . . . . . . . . 13
β’ ((πΊ β π β§ π β π) β dom π· β ((BaseβπΊ) Γ (BaseβπΊ))) |
22 | 21 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΊ β π β§ π β π) β§ π· β βͺ ran
βMet) β dom π·
β ((BaseβπΊ)
Γ (BaseβπΊ))) |
23 | | dmss 5862 |
. . . . . . . . . . . 12
β’ (dom
π· β
((BaseβπΊ) Γ
(BaseβπΊ)) β dom
dom π· β dom
((BaseβπΊ) Γ
(BaseβπΊ))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
β’ (((πΊ β π β§ π β π) β§ π· β βͺ ran
βMet) β dom dom π· β dom ((BaseβπΊ) Γ (BaseβπΊ))) |
25 | | dmxpid 5889 |
. . . . . . . . . . 11
β’ dom
((BaseβπΊ) Γ
(BaseβπΊ)) =
(BaseβπΊ) |
26 | 24, 25 | sseqtrdi 3998 |
. . . . . . . . . 10
β’ (((πΊ β π β§ π β π) β§ π· β βͺ ran
βMet) β dom dom π· β (BaseβπΊ)) |
27 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((πΊ β π β§ π β π) β§ π· β βͺ ran
βMet) β π· β
βͺ ran βMet) |
28 | | xmetunirn 23713 |
. . . . . . . . . . . 12
β’ (π· β βͺ ran βMet β π· β (βMetβdom dom π·)) |
29 | 27, 28 | sylib 217 |
. . . . . . . . . . 11
β’ (((πΊ β π β§ π β π) β§ π· β βͺ ran
βMet) β π· β
(βMetβdom dom π·)) |
30 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
31 | 30 | mopnuni 23817 |
. . . . . . . . . . 11
β’ (π· β (βMetβdom
dom π·) β dom dom π· = βͺ
(MetOpenβπ·)) |
32 | 29, 31 | syl 17 |
. . . . . . . . . 10
β’ (((πΊ β π β§ π β π) β§ π· β βͺ ran
βMet) β dom dom π· = βͺ
(MetOpenβπ·)) |
33 | 1, 14 | tngbas 24021 |
. . . . . . . . . . 11
β’ (π β π β (BaseβπΊ) = (Baseβπ)) |
34 | 33 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((πΊ β π β§ π β π) β§ π· β βͺ ran
βMet) β (BaseβπΊ) = (Baseβπ)) |
35 | 26, 32, 34 | 3sstr3d 3994 |
. . . . . . . . 9
β’ (((πΊ β π β§ π β π) β§ π· β βͺ ran
βMet) β βͺ (MetOpenβπ·) β (Baseβπ)) |
36 | | sspwuni 5064 |
. . . . . . . . 9
β’
((MetOpenβπ·)
β π« (Baseβπ) β βͺ
(MetOpenβπ·) β
(Baseβπ)) |
37 | 35, 36 | sylibr 233 |
. . . . . . . 8
β’ (((πΊ β π β§ π β π) β§ π· β βͺ ran
βMet) β (MetOpenβπ·) β π« (Baseβπ)) |
38 | 37 | ex 414 |
. . . . . . 7
β’ ((πΊ β π β§ π β π) β (π· β βͺ ran
βMet β (MetOpenβπ·) β π« (Baseβπ))) |
39 | 7, 38 | syl5 34 |
. . . . . 6
β’ ((πΊ β π β§ π β π) β (π· β dom MetOpen β
(MetOpenβπ·) β
π« (Baseβπ))) |
40 | | ndmfv 6881 |
. . . . . . 7
β’ (Β¬
π· β dom MetOpen β
(MetOpenβπ·) =
β
) |
41 | | 0ss 4360 |
. . . . . . 7
β’ β
β π« (Baseβπ) |
42 | 40, 41 | eqsstrdi 4002 |
. . . . . 6
β’ (Β¬
π· β dom MetOpen β
(MetOpenβπ·) β
π« (Baseβπ)) |
43 | 39, 42 | pm2.61d1 180 |
. . . . 5
β’ ((πΊ β π β§ π β π) β (MetOpenβπ·) β π« (Baseβπ)) |
44 | 3, 43 | eqsstrid 3996 |
. . . 4
β’ ((πΊ β π β§ π β π) β π½ β π« (Baseβπ)) |
45 | 4, 44 | eqsstrrd 3987 |
. . 3
β’ ((πΊ β π β§ π β π) β (TopSetβπ) β π« (Baseβπ)) |
46 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
47 | | eqid 2733 |
. . . 4
β’
(TopSetβπ) =
(TopSetβπ) |
48 | 46, 47 | topnid 17325 |
. . 3
β’
((TopSetβπ)
β π« (Baseβπ) β (TopSetβπ) = (TopOpenβπ)) |
49 | 45, 48 | syl 17 |
. 2
β’ ((πΊ β π β§ π β π) β (TopSetβπ) = (TopOpenβπ)) |
50 | 4, 49 | eqtrd 2773 |
1
β’ ((πΊ β π β§ π β π) β π½ = (TopOpenβπ)) |