Step | Hyp | Ref
| Expression |
1 | | simplll 774 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β§ π¦ β π) β π· β (βMetβπ)) |
2 | | simplr 768 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β§ π¦ β π) β π₯ β π) |
3 | | simplr 768 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β π β π) |
4 | 3 | sselda 3943 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β§ π¦ β π) β π¦ β π) |
5 | | xmetcl 23606 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π₯ β π β§ π¦ β π) β (π₯π·π¦) β
β*) |
6 | 1, 2, 4, 5 | syl3anc 1372 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β§ π¦ β π) β (π₯π·π¦) β
β*) |
7 | | eqid 2738 |
. . . . . 6
β’ (π¦ β π β¦ (π₯π·π¦)) = (π¦ β π β¦ (π₯π·π¦)) |
8 | 6, 7 | fmptd 7057 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β (π¦ β π β¦ (π₯π·π¦)):πβΆβ*) |
9 | 8 | frnd 6672 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β ran (π¦ β π β¦ (π₯π·π¦)) β
β*) |
10 | | infxrcl 13181 |
. . . 4
β’ (ran
(π¦ β π β¦ (π₯π·π¦)) β β* β inf(ran
(π¦ β π β¦ (π₯π·π¦)), β*, < ) β
β*) |
11 | 9, 10 | syl 17 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < ) β
β*) |
12 | | xmetge0 23619 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π₯ β π β§ π¦ β π) β 0 β€ (π₯π·π¦)) |
13 | 1, 2, 4, 12 | syl3anc 1372 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β§ π¦ β π) β 0 β€ (π₯π·π¦)) |
14 | 13 | ralrimiva 3142 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β βπ¦ β π 0 β€ (π₯π·π¦)) |
15 | | ovex 7383 |
. . . . . . 7
β’ (π₯π·π¦) β V |
16 | 15 | rgenw 3067 |
. . . . . 6
β’
βπ¦ β
π (π₯π·π¦) β V |
17 | | breq2 5108 |
. . . . . . 7
β’ (π§ = (π₯π·π¦) β (0 β€ π§ β 0 β€ (π₯π·π¦))) |
18 | 7, 17 | ralrnmptw 7039 |
. . . . . 6
β’
(βπ¦ β
π (π₯π·π¦) β V β (βπ§ β ran (π¦ β π β¦ (π₯π·π¦))0 β€ π§ β βπ¦ β π 0 β€ (π₯π·π¦))) |
19 | 16, 18 | ax-mp 5 |
. . . . 5
β’
(βπ§ β
ran (π¦ β π β¦ (π₯π·π¦))0 β€ π§ β βπ¦ β π 0 β€ (π₯π·π¦)) |
20 | 14, 19 | sylibr 233 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β βπ§ β ran (π¦ β π β¦ (π₯π·π¦))0 β€ π§) |
21 | | 0xr 11136 |
. . . . 5
β’ 0 β
β* |
22 | | infxrgelb 13183 |
. . . . 5
β’ ((ran
(π¦ β π β¦ (π₯π·π¦)) β β* β§ 0 β
β*) β (0 β€ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < ) β
βπ§ β ran (π¦ β π β¦ (π₯π·π¦))0 β€ π§)) |
23 | 9, 21, 22 | sylancl 587 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β (0 β€ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < ) β
βπ§ β ran (π¦ β π β¦ (π₯π·π¦))0 β€ π§)) |
24 | 20, 23 | mpbird 257 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β 0 β€ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
25 | | elxrge0 13303 |
. . 3
β’ (inf(ran
(π¦ β π β¦ (π₯π·π¦)), β*, < ) β
(0[,]+β) β (inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < ) β
β* β§ 0 β€ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
))) |
26 | 11, 24, 25 | sylanbrc 584 |
. 2
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < ) β
(0[,]+β)) |
27 | | metdscn.f |
. 2
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
28 | 26, 27 | fmptd 7057 |
1
β’ ((π· β (βMetβπ) β§ π β π) β πΉ:πβΆ(0[,]+β)) |