Step | Hyp | Ref
| Expression |
1 | | df-psmet 13417 |
. . . . . . . . 9
β’ PsMet =
(π β V β¦ {π β (β*
βπ (π Γ π)) β£ βπ β π ((πππ) = 0 β§ βπ β π βπ β π (πππ) β€ ((πππ) +π (πππ)))}) |
2 | 1 | mptrcl 5598 |
. . . . . . . 8
β’ (π· β (PsMetβπ) β π β V) |
3 | | ispsmet 13793 |
. . . . . . . 8
β’ (π β V β (π· β (PsMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ β π ((ππ·π) = 0 β§ βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π)))))) |
4 | 2, 3 | syl 14 |
. . . . . . 7
β’ (π· β (PsMetβπ) β (π· β (PsMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ β π ((ππ·π) = 0 β§ βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π)))))) |
5 | 4 | ibi 176 |
. . . . . 6
β’ (π· β (PsMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ β π ((ππ·π) = 0 β§ βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π))))) |
6 | 5 | simprd 114 |
. . . . 5
β’ (π· β (PsMetβπ) β βπ β π ((ππ·π) = 0 β§ βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π)))) |
7 | 6 | r19.21bi 2565 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π β π) β ((ππ·π) = 0 β§ βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π)))) |
8 | 7 | simprd 114 |
. . 3
β’ ((π· β (PsMetβπ) β§ π β π) β βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π))) |
9 | 8 | ralrimiva 2550 |
. 2
β’ (π· β (PsMetβπ) β βπ β π βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π))) |
10 | | oveq1 5881 |
. . . . 5
β’ (π = π΄ β (ππ·π) = (π΄π·π)) |
11 | | oveq2 5882 |
. . . . . 6
β’ (π = π΄ β (ππ·π) = (ππ·π΄)) |
12 | 11 | oveq1d 5889 |
. . . . 5
β’ (π = π΄ β ((ππ·π) +π (ππ·π)) = ((ππ·π΄) +π (ππ·π))) |
13 | 10, 12 | breq12d 4016 |
. . . 4
β’ (π = π΄ β ((ππ·π) β€ ((ππ·π) +π (ππ·π)) β (π΄π·π) β€ ((ππ·π΄) +π (ππ·π)))) |
14 | | oveq2 5882 |
. . . . 5
β’ (π = π΅ β (π΄π·π) = (π΄π·π΅)) |
15 | | oveq2 5882 |
. . . . . 6
β’ (π = π΅ β (ππ·π) = (ππ·π΅)) |
16 | 15 | oveq2d 5890 |
. . . . 5
β’ (π = π΅ β ((ππ·π΄) +π (ππ·π)) = ((ππ·π΄) +π (ππ·π΅))) |
17 | 14, 16 | breq12d 4016 |
. . . 4
β’ (π = π΅ β ((π΄π·π) β€ ((ππ·π΄) +π (ππ·π)) β (π΄π·π΅) β€ ((ππ·π΄) +π (ππ·π΅)))) |
18 | | oveq1 5881 |
. . . . . 6
β’ (π = πΆ β (ππ·π΄) = (πΆπ·π΄)) |
19 | | oveq1 5881 |
. . . . . 6
β’ (π = πΆ β (ππ·π΅) = (πΆπ·π΅)) |
20 | 18, 19 | oveq12d 5892 |
. . . . 5
β’ (π = πΆ β ((ππ·π΄) +π (ππ·π΅)) = ((πΆπ·π΄) +π (πΆπ·π΅))) |
21 | 20 | breq2d 4015 |
. . . 4
β’ (π = πΆ β ((π΄π·π΅) β€ ((ππ·π΄) +π (ππ·π΅)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
22 | 13, 17, 21 | rspc3v 2857 |
. . 3
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (βπ β π βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
23 | 22 | 3comr 1211 |
. 2
β’ ((πΆ β π β§ π΄ β π β§ π΅ β π) β (βπ β π βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
24 | 9, 23 | mpan9 281 |
1
β’ ((π· β (PsMetβπ) β§ (πΆ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅))) |