Step | Hyp | Ref
| Expression |
1 | | 1xr 11215 |
. . 3
β’ 1 β
β* |
2 | | metnrmlem.1 |
. . . . . . 7
β’ (π β π· β (βMetβπ)) |
3 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ (π΄ β π β§ π΅ β π)) β π· β (βMetβπ)) |
4 | | metnrmlem.2 |
. . . . . . . . 9
β’ (π β π β (Clsdβπ½)) |
5 | 4 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π΄ β π β§ π΅ β π)) β π β (Clsdβπ½)) |
6 | | eqid 2737 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
7 | 6 | cldss 22383 |
. . . . . . . 8
β’ (π β (Clsdβπ½) β π β βͺ π½) |
8 | 5, 7 | syl 17 |
. . . . . . 7
β’ ((π β§ (π΄ β π β§ π΅ β π)) β π β βͺ π½) |
9 | | metdscn.j |
. . . . . . . . 9
β’ π½ = (MetOpenβπ·) |
10 | 9 | mopnuni 23797 |
. . . . . . . 8
β’ (π· β (βMetβπ) β π = βͺ π½) |
11 | 3, 10 | syl 17 |
. . . . . . 7
β’ ((π β§ (π΄ β π β§ π΅ β π)) β π = βͺ π½) |
12 | 8, 11 | sseqtrrd 3986 |
. . . . . 6
β’ ((π β§ (π΄ β π β§ π΅ β π)) β π β π) |
13 | | metdscn.f |
. . . . . . 7
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
14 | 13 | metdsf 24214 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π) β πΉ:πβΆ(0[,]+β)) |
15 | 3, 12, 14 | syl2anc 585 |
. . . . 5
β’ ((π β§ (π΄ β π β§ π΅ β π)) β πΉ:πβΆ(0[,]+β)) |
16 | | metnrmlem.3 |
. . . . . . . . 9
β’ (π β π β (Clsdβπ½)) |
17 | 16 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π΄ β π β§ π΅ β π)) β π β (Clsdβπ½)) |
18 | 6 | cldss 22383 |
. . . . . . . 8
β’ (π β (Clsdβπ½) β π β βͺ π½) |
19 | 17, 18 | syl 17 |
. . . . . . 7
β’ ((π β§ (π΄ β π β§ π΅ β π)) β π β βͺ π½) |
20 | 19, 11 | sseqtrrd 3986 |
. . . . . 6
β’ ((π β§ (π΄ β π β§ π΅ β π)) β π β π) |
21 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π΄ β π β§ π΅ β π)) β π΅ β π) |
22 | 20, 21 | sseldd 3946 |
. . . . 5
β’ ((π β§ (π΄ β π β§ π΅ β π)) β π΅ β π) |
23 | 15, 22 | ffvelcdmd 7037 |
. . . 4
β’ ((π β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΅) β (0[,]+β)) |
24 | | eliccxr 13353 |
. . . 4
β’ ((πΉβπ΅) β (0[,]+β) β (πΉβπ΅) β
β*) |
25 | 23, 24 | syl 17 |
. . 3
β’ ((π β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΅) β
β*) |
26 | | ifcl 4532 |
. . 3
β’ ((1
β β* β§ (πΉβπ΅) β β*) β if(1
β€ (πΉβπ΅), 1, (πΉβπ΅)) β
β*) |
27 | 1, 25, 26 | sylancr 588 |
. 2
β’ ((π β§ (π΄ β π β§ π΅ β π)) β if(1 β€ (πΉβπ΅), 1, (πΉβπ΅)) β
β*) |
28 | | simprl 770 |
. . . 4
β’ ((π β§ (π΄ β π β§ π΅ β π)) β π΄ β π) |
29 | 12, 28 | sseldd 3946 |
. . 3
β’ ((π β§ (π΄ β π β§ π΅ β π)) β π΄ β π) |
30 | | xmetcl 23687 |
. . 3
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β
β*) |
31 | 3, 29, 22, 30 | syl3anc 1372 |
. 2
β’ ((π β§ (π΄ β π β§ π΅ β π)) β (π΄π·π΅) β
β*) |
32 | | xrmin2 13098 |
. . 3
β’ ((1
β β* β§ (πΉβπ΅) β β*) β if(1
β€ (πΉβπ΅), 1, (πΉβπ΅)) β€ (πΉβπ΅)) |
33 | 1, 25, 32 | sylancr 588 |
. 2
β’ ((π β§ (π΄ β π β§ π΅ β π)) β if(1 β€ (πΉβπ΅), 1, (πΉβπ΅)) β€ (πΉβπ΅)) |
34 | 13 | metdstri 24217 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΅ β π β§ π΄ β π)) β (πΉβπ΅) β€ ((π΅π·π΄) +π (πΉβπ΄))) |
35 | 3, 12, 22, 29, 34 | syl22anc 838 |
. . 3
β’ ((π β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΅) β€ ((π΅π·π΄) +π (πΉβπ΄))) |
36 | | xmetsym 23703 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π΅ β π β§ π΄ β π) β (π΅π·π΄) = (π΄π·π΅)) |
37 | 3, 22, 29, 36 | syl3anc 1372 |
. . . . 5
β’ ((π β§ (π΄ β π β§ π΅ β π)) β (π΅π·π΄) = (π΄π·π΅)) |
38 | 13 | metds0 24216 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (πΉβπ΄) = 0) |
39 | 3, 12, 28, 38 | syl3anc 1372 |
. . . . 5
β’ ((π β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΄) = 0) |
40 | 37, 39 | oveq12d 7376 |
. . . 4
β’ ((π β§ (π΄ β π β§ π΅ β π)) β ((π΅π·π΄) +π (πΉβπ΄)) = ((π΄π·π΅) +π 0)) |
41 | 31 | xaddid1d 13163 |
. . . 4
β’ ((π β§ (π΄ β π β§ π΅ β π)) β ((π΄π·π΅) +π 0) = (π΄π·π΅)) |
42 | 40, 41 | eqtrd 2777 |
. . 3
β’ ((π β§ (π΄ β π β§ π΅ β π)) β ((π΅π·π΄) +π (πΉβπ΄)) = (π΄π·π΅)) |
43 | 35, 42 | breqtrd 5132 |
. 2
β’ ((π β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΅) β€ (π΄π·π΅)) |
44 | 27, 25, 31, 33, 43 | xrletrd 13082 |
1
β’ ((π β§ (π΄ β π β§ π΅ β π)) β if(1 β€ (πΉβπ΅), 1, (πΉβπ΅)) β€ (π΄π·π΅)) |