Step | Hyp | Ref
| Expression |
1 | | xmetf 24190 |
. 2
β’ (π· β (βMetβπ) β π·:(π Γ π)βΆβ*) |
2 | | xmet0 24203 |
. . . 4
β’ ((π· β (βMetβπ) β§ π₯ β π) β (π₯π·π₯) = 0) |
3 | | 3anrot 1097 |
. . . . . . . 8
β’ ((π§ β π β§ π₯ β π β§ π¦ β π) β (π₯ β π β§ π¦ β π β§ π§ β π)) |
4 | | xmettri2 24201 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ (π§ β π β§ π₯ β π β§ π¦ β π)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
5 | 3, 4 | sylan2br 594 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
6 | 5 | 3anassrs 1357 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
7 | 6 | ralrimiva 3140 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ π¦ β π) β βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
8 | 7 | ralrimiva 3140 |
. . . 4
β’ ((π· β (βMetβπ) β§ π₯ β π) β βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
9 | 2, 8 | jca 511 |
. . 3
β’ ((π· β (βMetβπ) β§ π₯ β π) β ((π₯π·π₯) = 0 β§ βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
10 | 9 | ralrimiva 3140 |
. 2
β’ (π· β (βMetβπ) β βπ₯ β π ((π₯π·π₯) = 0 β§ βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
11 | | elfvex 6923 |
. . 3
β’ (π· β (βMetβπ) β π β V) |
12 | | ispsmet 24165 |
. . 3
β’ (π β V β (π· β (PsMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π ((π₯π·π₯) = 0 β§ βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
13 | 11, 12 | syl 17 |
. 2
β’ (π· β (βMetβπ) β (π· β (PsMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π ((π₯π·π₯) = 0 β§ βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
14 | 1, 10, 13 | mpbir2and 710 |
1
β’ (π· β (βMetβπ) β π· β (PsMetβπ)) |