Step | Hyp | Ref
| Expression |
1 | | elfvex 6923 |
. . . . . . . 8
β’ (π· β (PsMetβπ) β π β V) |
2 | | ispsmet 24165 |
. . . . . . . 8
β’ (π β V β (π· β (PsMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ β π ((ππ·π) = 0 β§ βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π)))))) |
3 | 1, 2 | syl 17 |
. . . . . . 7
β’ (π· β (PsMetβπ) β (π· β (PsMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ β π ((ππ·π) = 0 β§ βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π)))))) |
4 | 3 | ibi 267 |
. . . . . 6
β’ (π· β (PsMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ β π ((ππ·π) = 0 β§ βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π))))) |
5 | 4 | simprd 495 |
. . . . 5
β’ (π· β (PsMetβπ) β βπ β π ((ππ·π) = 0 β§ βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π)))) |
6 | 5 | r19.21bi 3242 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π β π) β ((ππ·π) = 0 β§ βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π)))) |
7 | 6 | simprd 495 |
. . 3
β’ ((π· β (PsMetβπ) β§ π β π) β βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π))) |
8 | 7 | ralrimiva 3140 |
. 2
β’ (π· β (PsMetβπ) β βπ β π βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π))) |
9 | | oveq1 7412 |
. . . . 5
β’ (π = π΄ β (ππ·π) = (π΄π·π)) |
10 | | oveq2 7413 |
. . . . . 6
β’ (π = π΄ β (ππ·π) = (ππ·π΄)) |
11 | 10 | oveq1d 7420 |
. . . . 5
β’ (π = π΄ β ((ππ·π) +π (ππ·π)) = ((ππ·π΄) +π (ππ·π))) |
12 | 9, 11 | breq12d 5154 |
. . . 4
β’ (π = π΄ β ((ππ·π) β€ ((ππ·π) +π (ππ·π)) β (π΄π·π) β€ ((ππ·π΄) +π (ππ·π)))) |
13 | | oveq2 7413 |
. . . . 5
β’ (π = π΅ β (π΄π·π) = (π΄π·π΅)) |
14 | | oveq2 7413 |
. . . . . 6
β’ (π = π΅ β (ππ·π) = (ππ·π΅)) |
15 | 14 | oveq2d 7421 |
. . . . 5
β’ (π = π΅ β ((ππ·π΄) +π (ππ·π)) = ((ππ·π΄) +π (ππ·π΅))) |
16 | 13, 15 | breq12d 5154 |
. . . 4
β’ (π = π΅ β ((π΄π·π) β€ ((ππ·π΄) +π (ππ·π)) β (π΄π·π΅) β€ ((ππ·π΄) +π (ππ·π΅)))) |
17 | | oveq1 7412 |
. . . . . 6
β’ (π = πΆ β (ππ·π΄) = (πΆπ·π΄)) |
18 | | oveq1 7412 |
. . . . . 6
β’ (π = πΆ β (ππ·π΅) = (πΆπ·π΅)) |
19 | 17, 18 | oveq12d 7423 |
. . . . 5
β’ (π = πΆ β ((ππ·π΄) +π (ππ·π΅)) = ((πΆπ·π΄) +π (πΆπ·π΅))) |
20 | 19 | breq2d 5153 |
. . . 4
β’ (π = πΆ β ((π΄π·π΅) β€ ((ππ·π΄) +π (ππ·π΅)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
21 | 12, 16, 20 | rspc3v 3622 |
. . 3
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (βπ β π βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
22 | 21 | 3comr 1122 |
. 2
β’ ((πΆ β π β§ π΄ β π β§ π΅ β π) β (βπ β π βπ β π βπ β π (ππ·π) β€ ((ππ·π) +π (ππ·π)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅)))) |
23 | 8, 22 | mpan9 506 |
1
β’ ((π· β (PsMetβπ) β§ (πΆ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅))) |