Step | Hyp | Ref
| Expression |
1 | | metdscn.f |
. . . 4
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
2 | 1 | metdsf 24227 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π) β πΉ:πβΆ(0[,]+β)) |
3 | | iccssxr 13354 |
. . 3
β’
(0[,]+β) β β* |
4 | | fss 6690 |
. . 3
β’ ((πΉ:πβΆ(0[,]+β) β§ (0[,]+β)
β β*) β πΉ:πβΆβ*) |
5 | 2, 3, 4 | sylancl 587 |
. 2
β’ ((π· β (βMetβπ) β§ π β π) β πΉ:πβΆβ*) |
6 | | simprr 772 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β π β
β+) |
7 | 5 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β πΉ:πβΆβ*) |
8 | | simplrl 776 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β π§ β π) |
9 | 7, 8 | ffvelcdmd 7041 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β (πΉβπ§) β
β*) |
10 | | simprl 770 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β π€ β π) |
11 | 7, 10 | ffvelcdmd 7041 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β (πΉβπ€) β
β*) |
12 | | metdscn.c |
. . . . . . . . 9
β’ πΆ =
(distββ*π ) |
13 | 12 | xrsdsval 20857 |
. . . . . . . 8
β’ (((πΉβπ§) β β* β§ (πΉβπ€) β β*) β ((πΉβπ§)πΆ(πΉβπ€)) = if((πΉβπ§) β€ (πΉβπ€), ((πΉβπ€) +π
-π(πΉβπ§)), ((πΉβπ§) +π
-π(πΉβπ€)))) |
14 | 9, 11, 13 | syl2anc 585 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β ((πΉβπ§)πΆ(πΉβπ€)) = if((πΉβπ§) β€ (πΉβπ€), ((πΉβπ€) +π
-π(πΉβπ§)), ((πΉβπ§) +π
-π(πΉβπ€)))) |
15 | | metdscn.j |
. . . . . . . . 9
β’ π½ = (MetOpenβπ·) |
16 | | metdscn.k |
. . . . . . . . 9
β’ πΎ = (MetOpenβπΆ) |
17 | | simplll 774 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β π· β (βMetβπ)) |
18 | | simpllr 775 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β π β π) |
19 | | simplrr 777 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β π β β+) |
20 | | xmetsym 23716 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π€ β π β§ π§ β π) β (π€π·π§) = (π§π·π€)) |
21 | 17, 10, 8, 20 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β (π€π·π§) = (π§π·π€)) |
22 | | simprr 772 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β (π§π·π€) < π) |
23 | 21, 22 | eqbrtrd 5132 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β (π€π·π§) < π) |
24 | 1, 15, 12, 16, 17, 18, 10, 8, 19, 23 | metdscnlem 24234 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β ((πΉβπ€) +π
-π(πΉβπ§)) < π) |
25 | 1, 15, 12, 16, 17, 18, 8, 10, 19, 22 | metdscnlem 24234 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β ((πΉβπ§) +π
-π(πΉβπ€)) < π) |
26 | | breq1 5113 |
. . . . . . . . 9
β’ (((πΉβπ€) +π
-π(πΉβπ§)) = if((πΉβπ§) β€ (πΉβπ€), ((πΉβπ€) +π
-π(πΉβπ§)), ((πΉβπ§) +π
-π(πΉβπ€))) β (((πΉβπ€) +π
-π(πΉβπ§)) < π β if((πΉβπ§) β€ (πΉβπ€), ((πΉβπ€) +π
-π(πΉβπ§)), ((πΉβπ§) +π
-π(πΉβπ€))) < π)) |
27 | | breq1 5113 |
. . . . . . . . 9
β’ (((πΉβπ§) +π
-π(πΉβπ€)) = if((πΉβπ§) β€ (πΉβπ€), ((πΉβπ€) +π
-π(πΉβπ§)), ((πΉβπ§) +π
-π(πΉβπ€))) β (((πΉβπ§) +π
-π(πΉβπ€)) < π β if((πΉβπ§) β€ (πΉβπ€), ((πΉβπ€) +π
-π(πΉβπ§)), ((πΉβπ§) +π
-π(πΉβπ€))) < π)) |
28 | 26, 27 | ifboth 4530 |
. . . . . . . 8
β’ ((((πΉβπ€) +π
-π(πΉβπ§)) < π β§ ((πΉβπ§) +π
-π(πΉβπ€)) < π) β if((πΉβπ§) β€ (πΉβπ€), ((πΉβπ€) +π
-π(πΉβπ§)), ((πΉβπ§) +π
-π(πΉβπ€))) < π) |
29 | 24, 25, 28 | syl2anc 585 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β if((πΉβπ§) β€ (πΉβπ€), ((πΉβπ€) +π
-π(πΉβπ§)), ((πΉβπ§) +π
-π(πΉβπ€))) < π) |
30 | 14, 29 | eqbrtrd 5132 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ (π€ β π β§ (π§π·π€) < π)) β ((πΉβπ§)πΆ(πΉβπ€)) < π) |
31 | 30 | expr 458 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β§ π€ β π) β ((π§π·π€) < π β ((πΉβπ§)πΆ(πΉβπ€)) < π)) |
32 | 31 | ralrimiva 3144 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β
βπ€ β π ((π§π·π€) < π β ((πΉβπ§)πΆ(πΉβπ€)) < π)) |
33 | | breq2 5114 |
. . . . 5
β’ (π = π β ((π§π·π€) < π β (π§π·π€) < π)) |
34 | 33 | rspceaimv 3588 |
. . . 4
β’ ((π β β+
β§ βπ€ β
π ((π§π·π€) < π β ((πΉβπ§)πΆ(πΉβπ€)) < π)) β βπ β β+ βπ€ β π ((π§π·π€) < π β ((πΉβπ§)πΆ(πΉβπ€)) < π)) |
35 | 6, 32, 34 | syl2anc 585 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π β β+)) β
βπ β
β+ βπ€ β π ((π§π·π€) < π β ((πΉβπ§)πΆ(πΉβπ€)) < π)) |
36 | 35 | ralrimivva 3198 |
. 2
β’ ((π· β (βMetβπ) β§ π β π) β βπ§ β π βπ β β+ βπ β β+
βπ€ β π ((π§π·π€) < π β ((πΉβπ§)πΆ(πΉβπ€)) < π)) |
37 | | simpl 484 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π) β π· β (βMetβπ)) |
38 | 12 | xrsxmet 24188 |
. . 3
β’ πΆ β
(βMetββ*) |
39 | 15, 16 | metcn 23915 |
. . 3
β’ ((π· β (βMetβπ) β§ πΆ β
(βMetββ*)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆβ* β§
βπ§ β π βπ β β+ βπ β β+
βπ€ β π ((π§π·π€) < π β ((πΉβπ§)πΆ(πΉβπ€)) < π)))) |
40 | 37, 38, 39 | sylancl 587 |
. 2
β’ ((π· β (βMetβπ) β§ π β π) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆβ* β§
βπ§ β π βπ β β+ βπ β β+
βπ€ β π ((π§π·π€) < π β ((πΉβπ§)πΆ(πΉβπ€)) < π)))) |
41 | 5, 36, 40 | mpbir2and 712 |
1
β’ ((π· β (βMetβπ) β§ π β π) β πΉ β (π½ Cn πΎ)) |