Step | Hyp | Ref
| Expression |
1 | | breq1 5113 |
. . . . 5
β’ (π΄ = -β β (π΄ < (πΉβπ₯) β -β < (πΉβπ₯))) |
2 | 1 | rabbidv 3418 |
. . . 4
β’ (π΄ = -β β {π₯ β π· β£ π΄ < (πΉβπ₯)} = {π₯ β π· β£ -β < (πΉβπ₯)}) |
3 | | smfpimgtxr.d |
. . . . . . 7
β’ π· = dom πΉ |
4 | | smfpimgtxr.x |
. . . . . . . 8
β’
β²π₯πΉ |
5 | 4 | nfdm 5911 |
. . . . . . 7
β’
β²π₯dom
πΉ |
6 | 3, 5 | nfcxfr 2906 |
. . . . . 6
β’
β²π₯π· |
7 | | nfcv 2908 |
. . . . . 6
β’
β²π¦π· |
8 | | nfv 1918 |
. . . . . 6
β’
β²π¦-β
< (πΉβπ₯) |
9 | | nfcv 2908 |
. . . . . . 7
β’
β²π₯-β |
10 | | nfcv 2908 |
. . . . . . 7
β’
β²π₯
< |
11 | | nfcv 2908 |
. . . . . . . 8
β’
β²π₯π¦ |
12 | 4, 11 | nffv 6857 |
. . . . . . 7
β’
β²π₯(πΉβπ¦) |
13 | 9, 10, 12 | nfbr 5157 |
. . . . . 6
β’
β²π₯-β
< (πΉβπ¦) |
14 | | fveq2 6847 |
. . . . . . 7
β’ (π₯ = π¦ β (πΉβπ₯) = (πΉβπ¦)) |
15 | 14 | breq2d 5122 |
. . . . . 6
β’ (π₯ = π¦ β (-β < (πΉβπ₯) β -β < (πΉβπ¦))) |
16 | 6, 7, 8, 13, 15 | cbvrabw 3442 |
. . . . 5
β’ {π₯ β π· β£ -β < (πΉβπ₯)} = {π¦ β π· β£ -β < (πΉβπ¦)} |
17 | | nfv 1918 |
. . . . . 6
β’
β²π¦π |
18 | | smfpimgtxr.s |
. . . . . . . 8
β’ (π β π β SAlg) |
19 | | smfpimgtxr.f |
. . . . . . . 8
β’ (π β πΉ β (SMblFnβπ)) |
20 | 18, 19, 3 | smff 45047 |
. . . . . . 7
β’ (π β πΉ:π·βΆβ) |
21 | 20 | ffvelcdmda 7040 |
. . . . . 6
β’ ((π β§ π¦ β π·) β (πΉβπ¦) β β) |
22 | 17, 21 | pimgtmnf 45038 |
. . . . 5
β’ (π β {π¦ β π· β£ -β < (πΉβπ¦)} = π·) |
23 | 16, 22 | eqtrid 2789 |
. . . 4
β’ (π β {π₯ β π· β£ -β < (πΉβπ₯)} = π·) |
24 | 2, 23 | sylan9eqr 2799 |
. . 3
β’ ((π β§ π΄ = -β) β {π₯ β π· β£ π΄ < (πΉβπ₯)} = π·) |
25 | 18, 19, 3 | smfdmss 45048 |
. . . . 5
β’ (π β π· β βͺ π) |
26 | 18, 25 | subsaluni 44675 |
. . . 4
β’ (π β π· β (π βΎt π·)) |
27 | 26 | adantr 482 |
. . 3
β’ ((π β§ π΄ = -β) β π· β (π βΎt π·)) |
28 | 24, 27 | eqeltrd 2838 |
. 2
β’ ((π β§ π΄ = -β) β {π₯ β π· β£ π΄ < (πΉβπ₯)} β (π βΎt π·)) |
29 | | breq1 5113 |
. . . . . . 7
β’ (π΄ = +β β (π΄ < (πΉβπ₯) β +β < (πΉβπ₯))) |
30 | 29 | rabbidv 3418 |
. . . . . 6
β’ (π΄ = +β β {π₯ β π· β£ π΄ < (πΉβπ₯)} = {π₯ β π· β£ +β < (πΉβπ₯)}) |
31 | 4, 6, 20 | pimgtpnf2f 45020 |
. . . . . 6
β’ (π β {π₯ β π· β£ +β < (πΉβπ₯)} = β
) |
32 | 30, 31 | sylan9eqr 2799 |
. . . . 5
β’ ((π β§ π΄ = +β) β {π₯ β π· β£ π΄ < (πΉβπ₯)} = β
) |
33 | 19 | dmexd 7847 |
. . . . . . . . 9
β’ (π β dom πΉ β V) |
34 | 3, 33 | eqeltrid 2842 |
. . . . . . . 8
β’ (π β π· β V) |
35 | | eqid 2737 |
. . . . . . . 8
β’ (π βΎt π·) = (π βΎt π·) |
36 | 18, 34, 35 | subsalsal 44674 |
. . . . . . 7
β’ (π β (π βΎt π·) β SAlg) |
37 | 36 | 0sald 44665 |
. . . . . 6
β’ (π β β
β (π βΎt π·)) |
38 | 37 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ = +β) β β
β (π βΎt π·)) |
39 | 32, 38 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π΄ = +β) β {π₯ β π· β£ π΄ < (πΉβπ₯)} β (π βΎt π·)) |
40 | 39 | adantlr 714 |
. . 3
β’ (((π β§ π΄ β -β) β§ π΄ = +β) β {π₯ β π· β£ π΄ < (πΉβπ₯)} β (π βΎt π·)) |
41 | | simpll 766 |
. . . 4
β’ (((π β§ π΄ β -β) β§ Β¬ π΄ = +β) β π) |
42 | | smfpimgtxr.a |
. . . . . 6
β’ (π β π΄ β
β*) |
43 | 41, 42 | syl 17 |
. . . . 5
β’ (((π β§ π΄ β -β) β§ Β¬ π΄ = +β) β π΄ β
β*) |
44 | | simplr 768 |
. . . . 5
β’ (((π β§ π΄ β -β) β§ Β¬ π΄ = +β) β π΄ β -β) |
45 | | neqne 2952 |
. . . . . 6
β’ (Β¬
π΄ = +β β π΄ β +β) |
46 | 45 | adantl 483 |
. . . . 5
β’ (((π β§ π΄ β -β) β§ Β¬ π΄ = +β) β π΄ β +β) |
47 | 43, 44, 46 | xrred 43673 |
. . . 4
β’ (((π β§ π΄ β -β) β§ Β¬ π΄ = +β) β π΄ β
β) |
48 | 18 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ β β) β π β SAlg) |
49 | 19 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ β β) β πΉ β (SMblFnβπ)) |
50 | | simpr 486 |
. . . . 5
β’ ((π β§ π΄ β β) β π΄ β β) |
51 | 4, 48, 49, 3, 50 | smfpreimagtf 45083 |
. . . 4
β’ ((π β§ π΄ β β) β {π₯ β π· β£ π΄ < (πΉβπ₯)} β (π βΎt π·)) |
52 | 41, 47, 51 | syl2anc 585 |
. . 3
β’ (((π β§ π΄ β -β) β§ Β¬ π΄ = +β) β {π₯ β π· β£ π΄ < (πΉβπ₯)} β (π βΎt π·)) |
53 | 40, 52 | pm2.61dan 812 |
. 2
β’ ((π β§ π΄ β -β) β {π₯ β π· β£ π΄ < (πΉβπ₯)} β (π βΎt π·)) |
54 | 28, 53 | pm2.61dane 3033 |
1
β’ (π β {π₯ β π· β£ π΄ < (πΉβπ₯)} β (π βΎt π·)) |