Step | Hyp | Ref
| Expression |
1 | | xmetcl 23837 |
. 2
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β
β*) |
2 | | xmetcl 23837 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β π β§ π΄ β π) β (π΅π·π΄) β
β*) |
3 | 2 | 3com23 1127 |
. 2
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΅π·π΄) β
β*) |
4 | | simp1 1137 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β π· β (βMetβπ)) |
5 | | simp3 1139 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β π΅ β π) |
6 | | simp2 1138 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β π΄ β π) |
7 | | xmettri2 23846 |
. . . 4
β’ ((π· β (βMetβπ) β§ (π΅ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((π΅π·π΄) +π (π΅π·π΅))) |
8 | 4, 5, 6, 5, 7 | syl13anc 1373 |
. . 3
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β€ ((π΅π·π΄) +π (π΅π·π΅))) |
9 | | xmet0 23848 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π΅ β π) β (π΅π·π΅) = 0) |
10 | 9 | 3adant2 1132 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΅π·π΅) = 0) |
11 | 10 | oveq2d 7425 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΅π·π΄) +π (π΅π·π΅)) = ((π΅π·π΄) +π 0)) |
12 | 2 | xaddridd 13222 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π΅ β π β§ π΄ β π) β ((π΅π·π΄) +π 0) = (π΅π·π΄)) |
13 | 12 | 3com23 1127 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΅π·π΄) +π 0) = (π΅π·π΄)) |
14 | 11, 13 | eqtrd 2773 |
. . 3
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΅π·π΄) +π (π΅π·π΅)) = (π΅π·π΄)) |
15 | 8, 14 | breqtrd 5175 |
. 2
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β€ (π΅π·π΄)) |
16 | | xmettri2 23846 |
. . . 4
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΅ β π β§ π΄ β π)) β (π΅π·π΄) β€ ((π΄π·π΅) +π (π΄π·π΄))) |
17 | 4, 6, 5, 6, 16 | syl13anc 1373 |
. . 3
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΅π·π΄) β€ ((π΄π·π΅) +π (π΄π·π΄))) |
18 | | xmet0 23848 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π΄ β π) β (π΄π·π΄) = 0) |
19 | 18 | 3adant3 1133 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΄) = 0) |
20 | 19 | oveq2d 7425 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅) +π (π΄π·π΄)) = ((π΄π·π΅) +π 0)) |
21 | 1 | xaddridd 13222 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅) +π 0) = (π΄π·π΅)) |
22 | 20, 21 | eqtrd 2773 |
. . 3
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅) +π (π΄π·π΄)) = (π΄π·π΅)) |
23 | 17, 22 | breqtrd 5175 |
. 2
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΅π·π΄) β€ (π΄π·π΅)) |
24 | 1, 3, 15, 23 | xrletrid 13134 |
1
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (π΅π·π΄)) |