Step | Hyp | Ref
| Expression |
1 | | elfvdm 6880 |
. . . . . . 7
β’ (π· β (βMetβπ) β π β dom βMet) |
2 | | isxmet 23693 |
. . . . . . 7
β’ (π β dom βMet β
(π· β
(βMetβπ) β
(π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (π· β (βMetβπ) β (π· β (βMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
4 | 3 | ibi 267 |
. . . . 5
β’ (π· β (βMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))))) |
5 | | simpr 486 |
. . . . . 6
β’ ((((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
6 | 5 | 2ralimi 3123 |
. . . . 5
β’
(βπ₯ β
π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β βπ₯ β π βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
7 | 4, 6 | simpl2im 505 |
. . . 4
β’ (π· β (βMetβπ) β βπ₯ β π βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
8 | | oveq1 7365 |
. . . . . 6
β’ (π₯ = π΄ β (π₯π·π¦) = (π΄π·π¦)) |
9 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = π΄ β (π§π·π₯) = (π§π·π΄)) |
10 | 9 | oveq1d 7373 |
. . . . . 6
β’ (π₯ = π΄ β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·π΄) +π (π§π·π¦))) |
11 | 8, 10 | breq12d 5119 |
. . . . 5
β’ (π₯ = π΄ β ((π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)) β (π΄π·π¦) β€ ((π§π·π΄) +π (π§π·π¦)))) |
12 | | oveq2 7366 |
. . . . . 6
β’ (π¦ = π΅ β (π΄π·π¦) = (π΄π·π΅)) |
13 | | oveq2 7366 |
. . . . . . 7
β’ (π¦ = π΅ β (π§π·π¦) = (π§π·π΅)) |
14 | 13 | oveq2d 7374 |
. . . . . 6
β’ (π¦ = π΅ β ((π§π·π΄) +π (π§π·π¦)) = ((π§π·π΄) +π (π§π·π΅))) |
15 | 12, 14 | breq12d 5119 |
. . . . 5
β’ (π¦ = π΅ β ((π΄π·π¦) β€ ((π§π·π΄) +π (π§π·π¦)) β (π΄π·π΅) β€ ((π§π·π΄) +π (π§π·π΅)))) |
16 | | oveq1 7365 |
. . . . . . 7
β’ (π§ = πΆ β (π§π·π΄) = (πΆπ·π΄)) |
17 | | oveq1 7365 |
. . . . . . 7
β’ (π§ = πΆ β (π§π·π΅) = (πΆπ·π΅)) |
18 | 16, 17 | oveq12d 7376 |
. . . . . 6
β’ (π§ = πΆ β ((π§π·π΄) +π (π§π·π΅)) = ((πΆπ·π΄) +π (πΆπ·π΅))) |
19 | 18 | breq2d 5118 |
. . . . 5
β’ (π§ = πΆ β ((π΄π·π΅) β€ ((π§π·π΄) +π (π§π·π΅)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
20 | 11, 15, 19 | rspc3v 3592 |
. . . 4
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (βπ₯ β π βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
21 | 7, 20 | syl5 34 |
. . 3
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (π· β (βMetβπ) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
22 | 21 | 3comr 1126 |
. 2
β’ ((πΆ β π β§ π΄ β π β§ π΅ β π) β (π· β (βMetβπ) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
23 | 22 | impcom 409 |
1
β’ ((π· β (βMetβπ) β§ (πΆ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅))) |