Step | Hyp | Ref
| Expression |
1 | | xmetrel 13882 |
. . . . . . . 8
β’ Rel
βMet |
2 | | relelfvdm 5549 |
. . . . . . . 8
β’ ((Rel
βMet β§ π· β
(βMetβπ))
β π β dom
βMet) |
3 | 1, 2 | mpan 424 |
. . . . . . 7
β’ (π· β (βMetβπ) β π β dom βMet) |
4 | | isxmet 13884 |
. . . . . . 7
β’ (π β dom βMet β
(π· β
(βMetβπ) β
(π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
5 | 3, 4 | syl 14 |
. . . . . 6
β’ (π· β (βMetβπ) β (π· β (βMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
6 | 5 | ibi 176 |
. . . . 5
β’ (π· β (βMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))))) |
7 | | simpr 110 |
. . . . . 6
β’ ((((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
8 | 7 | 2ralimi 2541 |
. . . . 5
β’
(βπ₯ β
π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β βπ₯ β π βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
9 | 6, 8 | simpl2im 386 |
. . . 4
β’ (π· β (βMetβπ) β βπ₯ β π βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
10 | | oveq1 5884 |
. . . . . 6
β’ (π₯ = π΄ β (π₯π·π¦) = (π΄π·π¦)) |
11 | | oveq2 5885 |
. . . . . . 7
β’ (π₯ = π΄ β (π§π·π₯) = (π§π·π΄)) |
12 | 11 | oveq1d 5892 |
. . . . . 6
β’ (π₯ = π΄ β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·π΄) +π (π§π·π¦))) |
13 | 10, 12 | breq12d 4018 |
. . . . 5
β’ (π₯ = π΄ β ((π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)) β (π΄π·π¦) β€ ((π§π·π΄) +π (π§π·π¦)))) |
14 | | oveq2 5885 |
. . . . . 6
β’ (π¦ = π΅ β (π΄π·π¦) = (π΄π·π΅)) |
15 | | oveq2 5885 |
. . . . . . 7
β’ (π¦ = π΅ β (π§π·π¦) = (π§π·π΅)) |
16 | 15 | oveq2d 5893 |
. . . . . 6
β’ (π¦ = π΅ β ((π§π·π΄) +π (π§π·π¦)) = ((π§π·π΄) +π (π§π·π΅))) |
17 | 14, 16 | breq12d 4018 |
. . . . 5
β’ (π¦ = π΅ β ((π΄π·π¦) β€ ((π§π·π΄) +π (π§π·π¦)) β (π΄π·π΅) β€ ((π§π·π΄) +π (π§π·π΅)))) |
18 | | oveq1 5884 |
. . . . . . 7
β’ (π§ = πΆ β (π§π·π΄) = (πΆπ·π΄)) |
19 | | oveq1 5884 |
. . . . . . 7
β’ (π§ = πΆ β (π§π·π΅) = (πΆπ·π΅)) |
20 | 18, 19 | oveq12d 5895 |
. . . . . 6
β’ (π§ = πΆ β ((π§π·π΄) +π (π§π·π΅)) = ((πΆπ·π΄) +π (πΆπ·π΅))) |
21 | 20 | breq2d 4017 |
. . . . 5
β’ (π§ = πΆ β ((π΄π·π΅) β€ ((π§π·π΄) +π (π§π·π΅)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
22 | 13, 17, 21 | rspc3v 2859 |
. . . 4
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (βπ₯ β π βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
23 | 9, 22 | syl5 32 |
. . 3
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (π· β (βMetβπ) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
24 | 23 | 3comr 1211 |
. 2
β’ ((πΆ β π β§ π΄ β π β§ π΅ β π) β (π· β (βMetβπ) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
25 | 24 | impcom 125 |
1
β’ ((π· β (βMetβπ) β§ (πΆ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅))) |