Step | Hyp | Ref
| Expression |
1 | | abvf.a |
. . . . . . 7
β’ π΄ = (AbsValβπ
) |
2 | 1 | abvrcl 20323 |
. . . . . 6
β’ (πΉ β π΄ β π
β Ring) |
3 | | abvf.b |
. . . . . . 7
β’ π΅ = (Baseβπ
) |
4 | | abvtri.p |
. . . . . . 7
β’ + =
(+gβπ
) |
5 | | eqid 2733 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
6 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ
) = (0gβπ
) |
7 | 1, 3, 4, 5, 6 | isabv 20321 |
. . . . . 6
β’ (π
β Ring β (πΉ β π΄ β (πΉ:π΅βΆ(0[,)+β) β§ βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = (0gβπ
)) β§ βπ¦ β π΅ ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))))) |
8 | 2, 7 | syl 17 |
. . . . 5
β’ (πΉ β π΄ β (πΉ β π΄ β (πΉ:π΅βΆ(0[,)+β) β§ βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = (0gβπ
)) β§ βπ¦ β π΅ ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))))) |
9 | 8 | ibi 267 |
. . . 4
β’ (πΉ β π΄ β (πΉ:π΅βΆ(0[,)+β) β§ βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = (0gβπ
)) β§ βπ¦ β π΅ ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))))) |
10 | | simpr 486 |
. . . . . . 7
β’ (((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) β (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
11 | 10 | ralimi 3083 |
. . . . . 6
β’
(βπ¦ β
π΅ ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) β βπ¦ β π΅ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
12 | 11 | adantl 483 |
. . . . 5
β’ ((((πΉβπ₯) = 0 β π₯ = (0gβπ
)) β§ βπ¦ β π΅ ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))) β βπ¦ β π΅ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
13 | 12 | ralimi 3083 |
. . . 4
β’
(βπ₯ β
π΅ (((πΉβπ₯) = 0 β π₯ = (0gβπ
)) β§ βπ¦ β π΅ ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))) β βπ₯ β π΅ βπ¦ β π΅ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
14 | 9, 13 | simpl2im 505 |
. . 3
β’ (πΉ β π΄ β βπ₯ β π΅ βπ¦ β π΅ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
15 | | fvoveq1 7384 |
. . . . 5
β’ (π₯ = π β (πΉβ(π₯ + π¦)) = (πΉβ(π + π¦))) |
16 | | fveq2 6846 |
. . . . . 6
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
17 | 16 | oveq1d 7376 |
. . . . 5
β’ (π₯ = π β ((πΉβπ₯) + (πΉβπ¦)) = ((πΉβπ) + (πΉβπ¦))) |
18 | 15, 17 | breq12d 5122 |
. . . 4
β’ (π₯ = π β ((πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)) β (πΉβ(π + π¦)) β€ ((πΉβπ) + (πΉβπ¦)))) |
19 | | oveq2 7369 |
. . . . . 6
β’ (π¦ = π β (π + π¦) = (π + π)) |
20 | 19 | fveq2d 6850 |
. . . . 5
β’ (π¦ = π β (πΉβ(π + π¦)) = (πΉβ(π + π))) |
21 | | fveq2 6846 |
. . . . . 6
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
22 | 21 | oveq2d 7377 |
. . . . 5
β’ (π¦ = π β ((πΉβπ) + (πΉβπ¦)) = ((πΉβπ) + (πΉβπ))) |
23 | 20, 22 | breq12d 5122 |
. . . 4
β’ (π¦ = π β ((πΉβ(π + π¦)) β€ ((πΉβπ) + (πΉβπ¦)) β (πΉβ(π + π)) β€ ((πΉβπ) + (πΉβπ)))) |
24 | 18, 23 | rspc2v 3592 |
. . 3
β’ ((π β π΅ β§ π β π΅) β (βπ₯ β π΅ βπ¦ β π΅ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)) β (πΉβ(π + π)) β€ ((πΉβπ) + (πΉβπ)))) |
25 | 14, 24 | syl5com 31 |
. 2
β’ (πΉ β π΄ β ((π β π΅ β§ π β π΅) β (πΉβ(π + π)) β€ ((πΉβπ) + (πΉβπ)))) |
26 | 25 | 3impib 1117 |
1
β’ ((πΉ β π΄ β§ π β π΅ β§ π β π΅) β (πΉβ(π + π)) β€ ((πΉβπ) + (πΉβπ))) |