Step | Hyp | Ref
| Expression |
1 | | simprr 772 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β π΅ β π) |
2 | | simpr 486 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π) β π β π) |
3 | 2 | sselda 3945 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π) β§ π΄ β π) β π΄ β π) |
4 | 3 | adantrr 716 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β π΄ β π) |
5 | 1, 4 | jca 513 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π΅ β π β§ π΄ β π)) |
6 | | metdscn.f |
. . . 4
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
7 | 6 | metdstri 24217 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΅ β π β§ π΄ β π)) β (πΉβπ΅) β€ ((π΅π·π΄) +π (πΉβπ΄))) |
8 | 5, 7 | syldan 592 |
. 2
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΅) β€ ((π΅π·π΄) +π (πΉβπ΄))) |
9 | | simpll 766 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β π· β (βMetβπ)) |
10 | | xmetsym 23703 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π΅ β π β§ π΄ β π) β (π΅π·π΄) = (π΄π·π΅)) |
11 | 9, 1, 4, 10 | syl3anc 1372 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π΅π·π΄) = (π΄π·π΅)) |
12 | 6 | metds0 24216 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (πΉβπ΄) = 0) |
13 | 12 | 3expa 1119 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π) β§ π΄ β π) β (πΉβπ΄) = 0) |
14 | 13 | adantrr 716 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΄) = 0) |
15 | 11, 14 | oveq12d 7376 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β ((π΅π·π΄) +π (πΉβπ΄)) = ((π΄π·π΅) +π 0)) |
16 | | xmetcl 23687 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β
β*) |
17 | 9, 4, 1, 16 | syl3anc 1372 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π΄π·π΅) β
β*) |
18 | 17 | xaddid1d 13163 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β ((π΄π·π΅) +π 0) = (π΄π·π΅)) |
19 | 15, 18 | eqtrd 2777 |
. 2
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β ((π΅π·π΄) +π (πΉβπ΄)) = (π΄π·π΅)) |
20 | 8, 19 | breqtrd 5132 |
1
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΅) β€ (π΄π·π΅)) |