Step | Hyp | Ref
| Expression |
1 | | simp1 997 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β π· β (PsMetβπ)) |
2 | | simp3 999 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β π΅ β π) |
3 | | simp2 998 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β π΄ β π) |
4 | | psmettri2 13913 |
. . . 4
β’ ((π· β (PsMetβπ) β§ (π΅ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((π΅π·π΄) +π (π΅π·π΅))) |
5 | 1, 2, 3, 2, 4 | syl13anc 1240 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β€ ((π΅π·π΄) +π (π΅π·π΅))) |
6 | | psmet0 13912 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π΅ β π) β (π΅π·π΅) = 0) |
7 | 6 | 3adant2 1016 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β (π΅π·π΅) = 0) |
8 | 7 | oveq2d 5893 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΅π·π΄) +π (π΅π·π΅)) = ((π΅π·π΄) +π 0)) |
9 | | psmetcl 13911 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π΅ β π β§ π΄ β π) β (π΅π·π΄) β
β*) |
10 | | xaddid1 9864 |
. . . . . 6
β’ ((π΅π·π΄) β β* β ((π΅π·π΄) +π 0) = (π΅π·π΄)) |
11 | 9, 10 | syl 14 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π΅ β π β§ π΄ β π) β ((π΅π·π΄) +π 0) = (π΅π·π΄)) |
12 | 11 | 3com23 1209 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΅π·π΄) +π 0) = (π΅π·π΄)) |
13 | 8, 12 | eqtrd 2210 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΅π·π΄) +π (π΅π·π΅)) = (π΅π·π΄)) |
14 | 5, 13 | breqtrd 4031 |
. 2
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β€ (π΅π·π΄)) |
15 | | psmettri2 13913 |
. . . 4
β’ ((π· β (PsMetβπ) β§ (π΄ β π β§ π΅ β π β§ π΄ β π)) β (π΅π·π΄) β€ ((π΄π·π΅) +π (π΄π·π΄))) |
16 | 1, 3, 2, 3, 15 | syl13anc 1240 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β (π΅π·π΄) β€ ((π΄π·π΅) +π (π΄π·π΄))) |
17 | | psmet0 13912 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π΄ β π) β (π΄π·π΄) = 0) |
18 | 17 | 3adant3 1017 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΄) = 0) |
19 | 18 | oveq2d 5893 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅) +π (π΄π·π΄)) = ((π΄π·π΅) +π 0)) |
20 | | psmetcl 13911 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β
β*) |
21 | | xaddid1 9864 |
. . . . 5
β’ ((π΄π·π΅) β β* β ((π΄π·π΅) +π 0) = (π΄π·π΅)) |
22 | 20, 21 | syl 14 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅) +π 0) = (π΄π·π΅)) |
23 | 19, 22 | eqtrd 2210 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅) +π (π΄π·π΄)) = (π΄π·π΅)) |
24 | 16, 23 | breqtrd 4031 |
. 2
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β (π΅π·π΄) β€ (π΄π·π΅)) |
25 | 9 | 3com23 1209 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β (π΅π·π΄) β
β*) |
26 | | xrletri3 9806 |
. . 3
β’ (((π΄π·π΅) β β* β§ (π΅π·π΄) β β*) β ((π΄π·π΅) = (π΅π·π΄) β ((π΄π·π΅) β€ (π΅π·π΄) β§ (π΅π·π΄) β€ (π΄π·π΅)))) |
27 | 20, 25, 26 | syl2anc 411 |
. 2
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅) = (π΅π·π΄) β ((π΄π·π΅) β€ (π΅π·π΄) β§ (π΅π·π΄) β€ (π΄π·π΅)))) |
28 | 14, 24, 27 | mpbir2and 944 |
1
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (π΅π·π΄)) |