Step | Hyp | Ref
| Expression |
1 | | breq2 5114 |
. . . . 5
β’ (π΄ = +β β ((πΉβπ₯) < π΄ β (πΉβπ₯) < +β)) |
2 | 1 | rabbidv 3418 |
. . . 4
β’ (π΄ = +β β {π₯ β π· β£ (πΉβπ₯) < π΄} = {π₯ β π· β£ (πΉβπ₯) < +β}) |
3 | | smfpimltxr.x |
. . . . 5
β’
β²π₯πΉ |
4 | | smfpimltxr.d |
. . . . . 6
β’ π· = dom πΉ |
5 | 3 | nfdm 5911 |
. . . . . 6
β’
β²π₯dom
πΉ |
6 | 4, 5 | nfcxfr 2906 |
. . . . 5
β’
β²π₯π· |
7 | | smfpimltxr.s |
. . . . . 6
β’ (π β π β SAlg) |
8 | | smfpimltxr.f |
. . . . . 6
β’ (π β πΉ β (SMblFnβπ)) |
9 | 7, 8, 4 | smff 45047 |
. . . . 5
β’ (π β πΉ:π·βΆβ) |
10 | 3, 6, 9 | pimltpnf2f 45027 |
. . . 4
β’ (π β {π₯ β π· β£ (πΉβπ₯) < +β} = π·) |
11 | 2, 10 | sylan9eqr 2799 |
. . 3
β’ ((π β§ π΄ = +β) β {π₯ β π· β£ (πΉβπ₯) < π΄} = π·) |
12 | 7, 8, 4 | smfdmss 45048 |
. . . . 5
β’ (π β π· β βͺ π) |
13 | 7, 12 | subsaluni 44675 |
. . . 4
β’ (π β π· β (π βΎt π·)) |
14 | 13 | adantr 482 |
. . 3
β’ ((π β§ π΄ = +β) β π· β (π βΎt π·)) |
15 | 11, 14 | eqeltrd 2838 |
. 2
β’ ((π β§ π΄ = +β) β {π₯ β π· β£ (πΉβπ₯) < π΄} β (π βΎt π·)) |
16 | | breq2 5114 |
. . . . . . . 8
β’ (π΄ = -β β ((πΉβπ₯) < π΄ β (πΉβπ₯) < -β)) |
17 | 16 | rabbidv 3418 |
. . . . . . 7
β’ (π΄ = -β β {π₯ β π· β£ (πΉβπ₯) < π΄} = {π₯ β π· β£ (πΉβπ₯) < -β}) |
18 | 17 | adantl 483 |
. . . . . 6
β’ ((π β§ π΄ = -β) β {π₯ β π· β£ (πΉβπ₯) < π΄} = {π₯ β π· β£ (πΉβπ₯) < -β}) |
19 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ = -β) β πΉ:π·βΆβ) |
20 | 3, 6, 19 | pimltmnf2f 45012 |
. . . . . 6
β’ ((π β§ π΄ = -β) β {π₯ β π· β£ (πΉβπ₯) < -β} = β
) |
21 | 18, 20 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π΄ = -β) β {π₯ β π· β£ (πΉβπ₯) < π΄} = β
) |
22 | 8 | dmexd 7847 |
. . . . . . . . 9
β’ (π β dom πΉ β V) |
23 | 4, 22 | eqeltrid 2842 |
. . . . . . . 8
β’ (π β π· β V) |
24 | | eqid 2737 |
. . . . . . . 8
β’ (π βΎt π·) = (π βΎt π·) |
25 | 7, 23, 24 | subsalsal 44674 |
. . . . . . 7
β’ (π β (π βΎt π·) β SAlg) |
26 | 25 | 0sald 44665 |
. . . . . 6
β’ (π β β
β (π βΎt π·)) |
27 | 26 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ = -β) β β
β (π βΎt π·)) |
28 | 21, 27 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π΄ = -β) β {π₯ β π· β£ (πΉβπ₯) < π΄} β (π βΎt π·)) |
29 | 28 | adantlr 714 |
. . 3
β’ (((π β§ π΄ β +β) β§ π΄ = -β) β {π₯ β π· β£ (πΉβπ₯) < π΄} β (π βΎt π·)) |
30 | | simpll 766 |
. . . 4
β’ (((π β§ π΄ β +β) β§ Β¬ π΄ = -β) β π) |
31 | | smfpimltxr.a |
. . . . . 6
β’ (π β π΄ β
β*) |
32 | 30, 31 | syl 17 |
. . . . 5
β’ (((π β§ π΄ β +β) β§ Β¬ π΄ = -β) β π΄ β
β*) |
33 | | neqne 2952 |
. . . . . 6
β’ (Β¬
π΄ = -β β π΄ β -β) |
34 | 33 | adantl 483 |
. . . . 5
β’ (((π β§ π΄ β +β) β§ Β¬ π΄ = -β) β π΄ β -β) |
35 | | simplr 768 |
. . . . 5
β’ (((π β§ π΄ β +β) β§ Β¬ π΄ = -β) β π΄ β +β) |
36 | 32, 34, 35 | xrred 43673 |
. . . 4
β’ (((π β§ π΄ β +β) β§ Β¬ π΄ = -β) β π΄ β
β) |
37 | 7 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ β β) β π β SAlg) |
38 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ β β) β πΉ β (SMblFnβπ)) |
39 | | simpr 486 |
. . . . 5
β’ ((π β§ π΄ β β) β π΄ β β) |
40 | 3, 37, 38, 4, 39 | smfpreimaltf 45051 |
. . . 4
β’ ((π β§ π΄ β β) β {π₯ β π· β£ (πΉβπ₯) < π΄} β (π βΎt π·)) |
41 | 30, 36, 40 | syl2anc 585 |
. . 3
β’ (((π β§ π΄ β +β) β§ Β¬ π΄ = -β) β {π₯ β π· β£ (πΉβπ₯) < π΄} β (π βΎt π·)) |
42 | 29, 41 | pm2.61dan 812 |
. 2
β’ ((π β§ π΄ β +β) β {π₯ β π· β£ (πΉβπ₯) < π΄} β (π βΎt π·)) |
43 | 15, 42 | pm2.61dane 3033 |
1
β’ (π β {π₯ β π· β£ (πΉβπ₯) < π΄} β (π βΎt π·)) |