Step | Hyp | Ref
| Expression |
1 | | xmetf 13990 |
. 2
β’ (π· β (βMetβπ) β π·:(π Γ π)βΆβ*) |
2 | | xmet0 14003 |
. . . 4
β’ ((π· β (βMetβπ) β§ π₯ β π) β (π₯π·π₯) = 0) |
3 | | 3anrot 983 |
. . . . . . . 8
β’ ((π§ β π β§ π₯ β π β§ π¦ β π) β (π₯ β π β§ π¦ β π β§ π§ β π)) |
4 | | xmettri2 14001 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ (π§ β π β§ π₯ β π β§ π¦ β π)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
5 | 3, 4 | sylan2br 288 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
6 | 5 | 3anassrs 1229 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
7 | 6 | ralrimiva 2550 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ π¦ β π) β βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
8 | 7 | ralrimiva 2550 |
. . . 4
β’ ((π· β (βMetβπ) β§ π₯ β π) β βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
9 | 2, 8 | jca 306 |
. . 3
β’ ((π· β (βMetβπ) β§ π₯ β π) β ((π₯π·π₯) = 0 β§ βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
10 | 9 | ralrimiva 2550 |
. 2
β’ (π· β (βMetβπ) β βπ₯ β π ((π₯π·π₯) = 0 β§ βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
11 | | xmetrel 13983 |
. . . 4
β’ Rel
βMet |
12 | | relelfvdm 5549 |
. . . . 5
β’ ((Rel
βMet β§ π· β
(βMetβπ))
β π β dom
βMet) |
13 | 12 | elexd 2752 |
. . . 4
β’ ((Rel
βMet β§ π· β
(βMetβπ))
β π β
V) |
14 | 11, 13 | mpan 424 |
. . 3
β’ (π· β (βMetβπ) β π β V) |
15 | | ispsmet 13963 |
. . 3
β’ (π β V β (π· β (PsMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π ((π₯π·π₯) = 0 β§ βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
16 | 14, 15 | syl 14 |
. 2
β’ (π· β (βMetβπ) β (π· β (PsMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π ((π₯π·π₯) = 0 β§ βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
17 | 1, 10, 16 | mpbir2and 944 |
1
β’ (π· β (βMetβπ) β π· β (PsMetβπ)) |