Step | Hyp | Ref
| Expression |
1 | | o1dm 15478 |
. . 3
β’ (πΉ β π(1) β dom
πΉ β
β) |
2 | | fdm 6725 |
. . . 4
β’ (πΉ:π΄βΆβ β dom πΉ = π΄) |
3 | 2 | sseq1d 4012 |
. . 3
β’ (πΉ:π΄βΆβ β (dom πΉ β β β π΄ β
β)) |
4 | 1, 3 | imbitrid 243 |
. 2
β’ (πΉ:π΄βΆβ β (πΉ β π(1) β π΄ β
β)) |
5 | | lo1dm 15467 |
. . 3
β’ ((abs
β πΉ) β
β€π(1) β dom (abs β πΉ) β β) |
6 | | absf 15288 |
. . . . . 6
β’
abs:ββΆβ |
7 | | fco 6740 |
. . . . . 6
β’
((abs:ββΆβ β§ πΉ:π΄βΆβ) β (abs β πΉ):π΄βΆβ) |
8 | 6, 7 | mpan 686 |
. . . . 5
β’ (πΉ:π΄βΆβ β (abs β πΉ):π΄βΆβ) |
9 | 8 | fdmd 6727 |
. . . 4
β’ (πΉ:π΄βΆβ β dom (abs β
πΉ) = π΄) |
10 | 9 | sseq1d 4012 |
. . 3
β’ (πΉ:π΄βΆβ β (dom (abs β
πΉ) β β β
π΄ β
β)) |
11 | 5, 10 | imbitrid 243 |
. 2
β’ (πΉ:π΄βΆβ β ((abs β πΉ) β β€π(1) β
π΄ β
β)) |
12 | | fvco3 6989 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆβ β§ π¦ β π΄) β ((abs β πΉ)βπ¦) = (absβ(πΉβπ¦))) |
13 | 12 | adantlr 711 |
. . . . . . . 8
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π¦ β π΄) β ((abs β πΉ)βπ¦) = (absβ(πΉβπ¦))) |
14 | 13 | breq1d 5157 |
. . . . . . 7
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π¦ β π΄) β (((abs β πΉ)βπ¦) β€ π β (absβ(πΉβπ¦)) β€ π)) |
15 | 14 | imbi2d 339 |
. . . . . 6
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π¦ β π΄) β ((π₯ β€ π¦ β ((abs β πΉ)βπ¦) β€ π) β (π₯ β€ π¦ β (absβ(πΉβπ¦)) β€ π))) |
16 | 15 | ralbidva 3173 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (βπ¦ β π΄ (π₯ β€ π¦ β ((abs β πΉ)βπ¦) β€ π) β βπ¦ β π΄ (π₯ β€ π¦ β (absβ(πΉβπ¦)) β€ π))) |
17 | 16 | 2rexbidv 3217 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β ((abs β πΉ)βπ¦) β€ π) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β (absβ(πΉβπ¦)) β€ π))) |
18 | | ello12 15464 |
. . . . 5
β’ (((abs
β πΉ):π΄βΆβ β§ π΄ β β) β ((abs
β πΉ) β
β€π(1) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β ((abs β πΉ)βπ¦) β€ π))) |
19 | 8, 18 | sylan 578 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β ((abs β πΉ) β β€π(1) β
βπ₯ β β
βπ β β
βπ¦ β π΄ (π₯ β€ π¦ β ((abs β πΉ)βπ¦) β€ π))) |
20 | | elo12 15475 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (πΉ β π(1) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β (absβ(πΉβπ¦)) β€ π))) |
21 | 17, 19, 20 | 3bitr4rd 311 |
. . 3
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (πΉ β π(1) β (abs β
πΉ) β
β€π(1))) |
22 | 21 | ex 411 |
. 2
β’ (πΉ:π΄βΆβ β (π΄ β β β (πΉ β π(1) β (abs β
πΉ) β
β€π(1)))) |
23 | 4, 11, 22 | pm5.21ndd 378 |
1
β’ (πΉ:π΄βΆβ β (πΉ β π(1) β (abs β
πΉ) β
β€π(1))) |