Step | Hyp | Ref
| Expression |
1 | | difss 4132 |
. . 3
β’ (β
β β) β β |
2 | | eldifi 4127 |
. . . . . . . 8
β’ (π₯ β (β β
β) β π₯ β
β) |
3 | 2 | imcld 15142 |
. . . . . . 7
β’ (π₯ β (β β
β) β (ββπ₯) β β) |
4 | 3 | recnd 11242 |
. . . . . 6
β’ (π₯ β (β β
β) β (ββπ₯) β β) |
5 | | eldifn 4128 |
. . . . . . 7
β’ (π₯ β (β β
β) β Β¬ π₯
β β) |
6 | | reim0b 15066 |
. . . . . . . . 9
β’ (π₯ β β β (π₯ β β β
(ββπ₯) =
0)) |
7 | 2, 6 | syl 17 |
. . . . . . . 8
β’ (π₯ β (β β
β) β (π₯ β
β β (ββπ₯) = 0)) |
8 | 7 | necon3bbid 2979 |
. . . . . . 7
β’ (π₯ β (β β
β) β (Β¬ π₯
β β β (ββπ₯) β 0)) |
9 | 5, 8 | mpbid 231 |
. . . . . 6
β’ (π₯ β (β β
β) β (ββπ₯) β 0) |
10 | 4, 9 | absrpcld 15395 |
. . . . 5
β’ (π₯ β (β β
β) β (absβ(ββπ₯)) β
β+) |
11 | | cnxmet 24289 |
. . . . . . . 8
β’ (abs
β β ) β (βMetββ) |
12 | 4 | abscld 15383 |
. . . . . . . . 9
β’ (π₯ β (β β
β) β (absβ(ββπ₯)) β β) |
13 | 12 | rexrd 11264 |
. . . . . . . 8
β’ (π₯ β (β β
β) β (absβ(ββπ₯)) β
β*) |
14 | | elbl 23894 |
. . . . . . . 8
β’ (((abs
β β ) β (βMetββ) β§ π₯ β β β§
(absβ(ββπ₯)) β β*) β (π¦ β (π₯(ballβ(abs β β
))(absβ(ββπ₯))) β (π¦ β β β§ (π₯(abs β β )π¦) < (absβ(ββπ₯))))) |
15 | 11, 2, 13, 14 | mp3an2i 1467 |
. . . . . . 7
β’ (π₯ β (β β
β) β (π¦ β
(π₯(ballβ(abs β
β ))(absβ(ββπ₯))) β (π¦ β β β§ (π₯(abs β β )π¦) < (absβ(ββπ₯))))) |
16 | | simprl 770 |
. . . . . . . . 9
β’ ((π₯ β (β β
β) β§ (π¦ β
β β§ (π₯(abs
β β )π¦) <
(absβ(ββπ₯)))) β π¦ β β) |
17 | 2 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β β
β) β§ π¦ β
β) β π₯ β
β) |
18 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (β β
β) β§ π¦ β
β) β π¦ β
β) |
19 | 18 | recnd 11242 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β β
β) β§ π¦ β
β) β π¦ β
β) |
20 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (abs
β β ) = (abs β β ) |
21 | 20 | cnmetdval 24287 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π¦ β β) β (π₯(abs β β )π¦) = (absβ(π₯ β π¦))) |
22 | 17, 19, 21 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π₯ β (β β
β) β§ π¦ β
β) β (π₯(abs
β β )π¦) =
(absβ(π₯ β π¦))) |
23 | 4 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (β β
β) β§ π¦ β
β) β (ββπ₯) β β) |
24 | 23 | abscld 15383 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β β
β) β§ π¦ β
β) β (absβ(ββπ₯)) β β) |
25 | 17, 19 | subcld 11571 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (β β
β) β§ π¦ β
β) β (π₯ β
π¦) β
β) |
26 | 25 | abscld 15383 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β β
β) β§ π¦ β
β) β (absβ(π₯ β π¦)) β β) |
27 | 17, 19 | imsubd 15164 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β (β β
β) β§ π¦ β
β) β (ββ(π₯ β π¦)) = ((ββπ₯) β (ββπ¦))) |
28 | | reim0 15065 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β β β
(ββπ¦) =
0) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β (β β
β) β§ π¦ β
β) β (ββπ¦) = 0) |
30 | 29 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β (β β
β) β§ π¦ β
β) β ((ββπ₯) β (ββπ¦)) = ((ββπ₯) β 0)) |
31 | 23 | subid1d 11560 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β (β β
β) β§ π¦ β
β) β ((ββπ₯) β 0) = (ββπ₯)) |
32 | 27, 30, 31 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β (β β
β) β§ π¦ β
β) β (ββ(π₯ β π¦)) = (ββπ₯)) |
33 | 32 | fveq2d 6896 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (β β
β) β§ π¦ β
β) β (absβ(ββ(π₯ β π¦))) = (absβ(ββπ₯))) |
34 | | absimle 15256 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π¦) β β β
(absβ(ββ(π₯ β π¦))) β€ (absβ(π₯ β π¦))) |
35 | 25, 34 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (β β
β) β§ π¦ β
β) β (absβ(ββ(π₯ β π¦))) β€ (absβ(π₯ β π¦))) |
36 | 33, 35 | eqbrtrrd 5173 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β β
β) β§ π¦ β
β) β (absβ(ββπ₯)) β€ (absβ(π₯ β π¦))) |
37 | 24, 26, 36 | lensymd 11365 |
. . . . . . . . . . . . . 14
β’ ((π₯ β (β β
β) β§ π¦ β
β) β Β¬ (absβ(π₯ β π¦)) < (absβ(ββπ₯))) |
38 | 22, 37 | eqnbrtrd 5167 |
. . . . . . . . . . . . 13
β’ ((π₯ β (β β
β) β§ π¦ β
β) β Β¬ (π₯(abs β β )π¦) < (absβ(ββπ₯))) |
39 | 38 | ex 414 |
. . . . . . . . . . . 12
β’ (π₯ β (β β
β) β (π¦ β
β β Β¬ (π₯(abs
β β )π¦) <
(absβ(ββπ₯)))) |
40 | 39 | con2d 134 |
. . . . . . . . . . 11
β’ (π₯ β (β β
β) β ((π₯(abs
β β )π¦) <
(absβ(ββπ₯)) β Β¬ π¦ β β)) |
41 | 40 | adantr 482 |
. . . . . . . . . 10
β’ ((π₯ β (β β
β) β§ π¦ β
β) β ((π₯(abs
β β )π¦) <
(absβ(ββπ₯)) β Β¬ π¦ β β)) |
42 | 41 | impr 456 |
. . . . . . . . 9
β’ ((π₯ β (β β
β) β§ (π¦ β
β β§ (π₯(abs
β β )π¦) <
(absβ(ββπ₯)))) β Β¬ π¦ β β) |
43 | 16, 42 | eldifd 3960 |
. . . . . . . 8
β’ ((π₯ β (β β
β) β§ (π¦ β
β β§ (π₯(abs
β β )π¦) <
(absβ(ββπ₯)))) β π¦ β (β β
β)) |
44 | 43 | ex 414 |
. . . . . . 7
β’ (π₯ β (β β
β) β ((π¦ β
β β§ (π₯(abs
β β )π¦) <
(absβ(ββπ₯))) β π¦ β (β β
β))) |
45 | 15, 44 | sylbid 239 |
. . . . . 6
β’ (π₯ β (β β
β) β (π¦ β
(π₯(ballβ(abs β
β ))(absβ(ββπ₯))) β π¦ β (β β
β))) |
46 | 45 | ssrdv 3989 |
. . . . 5
β’ (π₯ β (β β
β) β (π₯(ballβ(abs β β
))(absβ(ββπ₯))) β (β β
β)) |
47 | | oveq2 7417 |
. . . . . . 7
β’ (π¦ =
(absβ(ββπ₯)) β (π₯(ballβ(abs β β ))π¦) = (π₯(ballβ(abs β β
))(absβ(ββπ₯)))) |
48 | 47 | sseq1d 4014 |
. . . . . 6
β’ (π¦ =
(absβ(ββπ₯)) β ((π₯(ballβ(abs β β ))π¦) β (β β
β) β (π₯(ballβ(abs β β
))(absβ(ββπ₯))) β (β β
β))) |
49 | 48 | rspcev 3613 |
. . . . 5
β’
(((absβ(ββπ₯)) β β+ β§ (π₯(ballβ(abs β β
))(absβ(ββπ₯))) β (β β β)) β
βπ¦ β
β+ (π₯(ballβ(abs β β ))π¦) β (β β
β)) |
50 | 10, 46, 49 | syl2anc 585 |
. . . 4
β’ (π₯ β (β β
β) β βπ¦
β β+ (π₯(ballβ(abs β β ))π¦) β (β β
β)) |
51 | 50 | rgen 3064 |
. . 3
β’
βπ₯ β
(β β β)βπ¦ β β+ (π₯(ballβ(abs β β
))π¦) β (β
β β) |
52 | | recld2.1 |
. . . . . 6
β’ π½ =
(TopOpenββfld) |
53 | 52 | cnfldtopn 24298 |
. . . . 5
β’ π½ = (MetOpenβ(abs β
β )) |
54 | 53 | elmopn2 23951 |
. . . 4
β’ ((abs
β β ) β (βMetββ) β ((β β
β) β π½ β
((β β β) β β β§ βπ₯ β (β β β)βπ¦ β β+
(π₯(ballβ(abs β
β ))π¦) β
(β β β)))) |
55 | 11, 54 | ax-mp 5 |
. . 3
β’ ((β
β β) β π½
β ((β β β) β β β§ βπ₯ β (β β
β)βπ¦ β
β+ (π₯(ballβ(abs β β ))π¦) β (β β
β))) |
56 | 1, 51, 55 | mpbir2an 710 |
. 2
β’ (β
β β) β π½ |
57 | 52 | cnfldtop 24300 |
. . 3
β’ π½ β Top |
58 | | ax-resscn 11167 |
. . 3
β’ β
β β |
59 | 53 | mopnuni 23947 |
. . . . 5
β’ ((abs
β β ) β (βMetββ) β β = βͺ π½) |
60 | 11, 59 | ax-mp 5 |
. . . 4
β’ β =
βͺ π½ |
61 | 60 | iscld2 22532 |
. . 3
β’ ((π½ β Top β§ β
β β) β (β β (Clsdβπ½) β (β β β) β
π½)) |
62 | 57, 58, 61 | mp2an 691 |
. 2
β’ (β
β (Clsdβπ½)
β (β β β) β π½) |
63 | 56, 62 | mpbir 230 |
1
β’ β
β (Clsdβπ½) |