Step | Hyp | Ref
| Expression |
1 | | extoimad.2 |
. 2
β’ (π β βπ¦ β β (absβ(πΉβπ¦)) β€ πΆ) |
2 | | extoimad.1 |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
3 | 2 | ffvelcdmda 6989 |
. . . . 5
β’ ((π β§ π¦ β β) β (πΉβπ¦) β β) |
4 | 3 | recnd 11045 |
. . . 4
β’ ((π β§ π¦ β β) β (πΉβπ¦) β β) |
5 | 4 | abscld 15189 |
. . 3
β’ ((π β§ π¦ β β) β (absβ(πΉβπ¦)) β β) |
6 | | imaco 6165 |
. . . . . 6
β’ ((abs
β πΉ) β β)
= (abs β (πΉ β
β)) |
7 | 6 | a1i 11 |
. . . . 5
β’ (π β ((abs β πΉ) β β) = (abs
β (πΉ β
β))) |
8 | 7 | eleq2d 2822 |
. . . 4
β’ (π β (π₯ β ((abs β πΉ) β β) β π₯ β (abs β (πΉ β β)))) |
9 | | absf 15090 |
. . . . . . . . . . 11
β’
abs:ββΆβ |
10 | 9 | a1i 11 |
. . . . . . . . . 10
β’ (π β
abs:ββΆβ) |
11 | | ax-resscn 10970 |
. . . . . . . . . . 11
β’ β
β β |
12 | 11 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β
β) |
13 | 10, 12 | fssresd 6667 |
. . . . . . . . 9
β’ (π β (abs βΎ
β):ββΆβ) |
14 | 2, 13 | fco2d 41810 |
. . . . . . . 8
β’ (π β (abs β πΉ):ββΆβ) |
15 | 14 | ffnd 6627 |
. . . . . . 7
β’ (π β (abs β πΉ) Fn β) |
16 | | ssidd 3949 |
. . . . . . 7
β’ (π β β β
β) |
17 | 15, 16 | fvelimabd 6870 |
. . . . . 6
β’ (π β (π₯ β ((abs β πΉ) β β) β βπ¦ β β ((abs β
πΉ)βπ¦) = π₯)) |
18 | | eqcom 2743 |
. . . . . . . 8
β’ (((abs
β πΉ)βπ¦) = π₯ β π₯ = ((abs β πΉ)βπ¦)) |
19 | 18 | a1i 11 |
. . . . . . 7
β’ (π β (((abs β πΉ)βπ¦) = π₯ β π₯ = ((abs β πΉ)βπ¦))) |
20 | 19 | rexbidv 3172 |
. . . . . 6
β’ (π β (βπ¦ β β ((abs β πΉ)βπ¦) = π₯ β βπ¦ β β π₯ = ((abs β πΉ)βπ¦))) |
21 | 17, 20 | bitrd 280 |
. . . . 5
β’ (π β (π₯ β ((abs β πΉ) β β) β βπ¦ β β π₯ = ((abs β πΉ)βπ¦))) |
22 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β πΉ:ββΆβ) |
23 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β π¦ β β) |
24 | 22, 23 | fvco3d 6896 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β ((abs β πΉ)βπ¦) = (absβ(πΉβπ¦))) |
25 | 24 | eqcomd 2742 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (absβ(πΉβπ¦)) = ((abs β πΉ)βπ¦)) |
26 | 25 | eqeq2d 2747 |
. . . . . 6
β’ ((π β§ π¦ β β) β (π₯ = (absβ(πΉβπ¦)) β π₯ = ((abs β πΉ)βπ¦))) |
27 | 26 | rexbidva 3170 |
. . . . 5
β’ (π β (βπ¦ β β π₯ = (absβ(πΉβπ¦)) β βπ¦ β β π₯ = ((abs β πΉ)βπ¦))) |
28 | 21, 27 | bitr4d 283 |
. . . 4
β’ (π β (π₯ β ((abs β πΉ) β β) β βπ¦ β β π₯ = (absβ(πΉβπ¦)))) |
29 | 8, 28 | bitr3d 282 |
. . 3
β’ (π β (π₯ β (abs β (πΉ β β)) β βπ¦ β β π₯ = (absβ(πΉβπ¦)))) |
30 | | simpr 486 |
. . . 4
β’ ((π β§ π₯ = (absβ(πΉβπ¦))) β π₯ = (absβ(πΉβπ¦))) |
31 | 30 | breq1d 5091 |
. . 3
β’ ((π β§ π₯ = (absβ(πΉβπ¦))) β (π₯ β€ πΆ β (absβ(πΉβπ¦)) β€ πΆ)) |
32 | 5, 29, 31 | ralxfr2d 5342 |
. 2
β’ (π β (βπ₯ β (abs β (πΉ β β))π₯ β€ πΆ β βπ¦ β β (absβ(πΉβπ¦)) β€ πΆ)) |
33 | 1, 32 | mpbird 258 |
1
β’ (π β βπ₯ β (abs β (πΉ β β))π₯ β€ πΆ) |