Step | Hyp | Ref
| Expression |
1 | | smfinflem.g |
. . . 4
β’ πΊ = (π₯ β π· β¦ inf(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) |
2 | 1 | a1i 11 |
. . 3
β’ (π β πΊ = (π₯ β π· β¦ inf(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < ))) |
3 | | nfv 1917 |
. . . . 5
β’
β²π(π β§ π₯ β π·) |
4 | | smfinflem.m |
. . . . . . 7
β’ (π β π β β€) |
5 | | smfinflem.z |
. . . . . . 7
β’ π =
(β€β₯βπ) |
6 | 4, 5 | uzn0d 44214 |
. . . . . 6
β’ (π β π β β
) |
7 | 6 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β π·) β π β β
) |
8 | | smfinflem.s |
. . . . . . . . 9
β’ (π β π β SAlg) |
9 | 8 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β π) β π β SAlg) |
10 | | smfinflem.f |
. . . . . . . . 9
β’ (π β πΉ:πβΆ(SMblFnβπ)) |
11 | 10 | ffvelcdmda 7086 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΉβπ) β (SMblFnβπ)) |
12 | | eqid 2732 |
. . . . . . . 8
β’ dom
(πΉβπ) = dom (πΉβπ) |
13 | 9, 11, 12 | smff 45527 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
14 | 13 | adantlr 713 |
. . . . . 6
β’ (((π β§ π₯ β π·) β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
15 | | ssrab2 4077 |
. . . . . . . . . 10
β’ {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)} β β© π β π dom (πΉβπ) |
16 | | smfinflem.d |
. . . . . . . . . . . 12
β’ π· = {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)} |
17 | 16 | eleq2i 2825 |
. . . . . . . . . . 11
β’ (π₯ β π· β π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)}) |
18 | 17 | biimpi 215 |
. . . . . . . . . 10
β’ (π₯ β π· β π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)}) |
19 | 15, 18 | sselid 3980 |
. . . . . . . . 9
β’ (π₯ β π· β π₯ β β©
π β π dom (πΉβπ)) |
20 | 19 | adantr 481 |
. . . . . . . 8
β’ ((π₯ β π· β§ π β π) β π₯ β β©
π β π dom (πΉβπ)) |
21 | | simpr 485 |
. . . . . . . 8
β’ ((π₯ β π· β§ π β π) β π β π) |
22 | | eliinid 43882 |
. . . . . . . 8
β’ ((π₯ β β© π β π dom (πΉβπ) β§ π β π) β π₯ β dom (πΉβπ)) |
23 | 20, 21, 22 | syl2anc 584 |
. . . . . . 7
β’ ((π₯ β π· β§ π β π) β π₯ β dom (πΉβπ)) |
24 | 23 | adantll 712 |
. . . . . 6
β’ (((π β§ π₯ β π·) β§ π β π) β π₯ β dom (πΉβπ)) |
25 | 14, 24 | ffvelcdmd 7087 |
. . . . 5
β’ (((π β§ π₯ β π·) β§ π β π) β ((πΉβπ)βπ₯) β β) |
26 | | rabidim2 43873 |
. . . . . . 7
β’ (π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)} β βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)) |
27 | 18, 26 | syl 17 |
. . . . . 6
β’ (π₯ β π· β βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)) |
28 | 27 | adantl 482 |
. . . . 5
β’ ((π β§ π₯ β π·) β βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)) |
29 | 3, 7, 25, 28 | infnsuprnmpt 44033 |
. . . 4
β’ ((π β§ π₯ β π·) β inf(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < ) = -sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < )) |
30 | 29 | mpteq2dva 5248 |
. . 3
β’ (π β (π₯ β π· β¦ inf(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) = (π₯ β π· β¦ -sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < ))) |
31 | 2, 30 | eqtrd 2772 |
. 2
β’ (π β πΊ = (π₯ β π· β¦ -sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < ))) |
32 | | nfv 1917 |
. . 3
β’
β²π₯π |
33 | | fvex 6904 |
. . . . . . . 8
β’ (πΉβπ) β V |
34 | 33 | dmex 7904 |
. . . . . . 7
β’ dom
(πΉβπ) β V |
35 | 34 | rgenw 3065 |
. . . . . 6
β’
βπ β
π dom (πΉβπ) β V |
36 | 35 | a1i 11 |
. . . . 5
β’ (π β βπ β π dom (πΉβπ) β V) |
37 | 6, 36 | iinexd 43904 |
. . . 4
β’ (π β β© π β π dom (πΉβπ) β V) |
38 | 16, 37 | rabexd 5333 |
. . 3
β’ (π β π· β V) |
39 | 25 | renegcld 11643 |
. . . 4
β’ (((π β§ π₯ β π·) β§ π β π) β -((πΉβπ)βπ₯) β β) |
40 | | fveq2 6891 |
. . . . . . . . . . . 12
β’ (π€ = π₯ β ((πΉβπ)βπ€) = ((πΉβπ)βπ₯)) |
41 | 40 | breq2d 5160 |
. . . . . . . . . . 11
β’ (π€ = π₯ β (π§ β€ ((πΉβπ)βπ€) β π§ β€ ((πΉβπ)βπ₯))) |
42 | 41 | ralbidv 3177 |
. . . . . . . . . 10
β’ (π€ = π₯ β (βπ β π π§ β€ ((πΉβπ)βπ€) β βπ β π π§ β€ ((πΉβπ)βπ₯))) |
43 | 42 | rexbidv 3178 |
. . . . . . . . 9
β’ (π€ = π₯ β (βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ€) β βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ₯))) |
44 | | nfcv 2903 |
. . . . . . . . . . 11
β’
β²π€β© π β π dom (πΉβπ) |
45 | | nfcv 2903 |
. . . . . . . . . . . 12
β’
β²π₯π |
46 | | nfcv 2903 |
. . . . . . . . . . . . 13
β’
β²π₯(πΉβπ) |
47 | 46 | nfdm 5950 |
. . . . . . . . . . . 12
β’
β²π₯dom
(πΉβπ) |
48 | 45, 47 | nfiin 5028 |
. . . . . . . . . . 11
β’
β²π₯β© π β π dom (πΉβπ) |
49 | | nfv 1917 |
. . . . . . . . . . 11
β’
β²π€βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯) |
50 | | nfv 1917 |
. . . . . . . . . . 11
β’
β²π₯βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ€) |
51 | | nfcv 2903 |
. . . . . . . . . . . . 13
β’
β²πdom
(πΉβπ) |
52 | | nfcv 2903 |
. . . . . . . . . . . . . 14
β’
β²π(πΉβπ) |
53 | 52 | nfdm 5950 |
. . . . . . . . . . . . 13
β’
β²πdom
(πΉβπ) |
54 | | fveq2 6891 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΉβπ) = (πΉβπ)) |
55 | 54 | dmeqd 5905 |
. . . . . . . . . . . . 13
β’ (π = π β dom (πΉβπ) = dom (πΉβπ)) |
56 | 51, 53, 55 | cbviin 5040 |
. . . . . . . . . . . 12
β’ β© π β π dom (πΉβπ) = β© π β π dom (πΉβπ) |
57 | 56 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ = π€ β β©
π β π dom (πΉβπ) = β© π β π dom (πΉβπ)) |
58 | | fveq2 6891 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π€ β ((πΉβπ)βπ₯) = ((πΉβπ)βπ€)) |
59 | 58 | breq2d 5160 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π€ β (π¦ β€ ((πΉβπ)βπ₯) β π¦ β€ ((πΉβπ)βπ€))) |
60 | 59 | ralbidv 3177 |
. . . . . . . . . . . . . 14
β’ (π₯ = π€ β (βπ β π π¦ β€ ((πΉβπ)βπ₯) β βπ β π π¦ β€ ((πΉβπ)βπ€))) |
61 | | nfv 1917 |
. . . . . . . . . . . . . . . 16
β’
β²π π¦ β€ ((πΉβπ)βπ€) |
62 | | nfcv 2903 |
. . . . . . . . . . . . . . . . 17
β’
β²ππ¦ |
63 | | nfcv 2903 |
. . . . . . . . . . . . . . . . 17
β’
β²π
β€ |
64 | | nfcv 2903 |
. . . . . . . . . . . . . . . . . 18
β’
β²ππ€ |
65 | 52, 64 | nffv 6901 |
. . . . . . . . . . . . . . . . 17
β’
β²π((πΉβπ)βπ€) |
66 | 62, 63, 65 | nfbr 5195 |
. . . . . . . . . . . . . . . 16
β’
β²π π¦ β€ ((πΉβπ)βπ€) |
67 | 54 | fveq1d 6893 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((πΉβπ)βπ€) = ((πΉβπ)βπ€)) |
68 | 67 | breq2d 5160 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π¦ β€ ((πΉβπ)βπ€) β π¦ β€ ((πΉβπ)βπ€))) |
69 | 61, 66, 68 | cbvralw 3303 |
. . . . . . . . . . . . . . 15
β’
(βπ β
π π¦ β€ ((πΉβπ)βπ€) β βπ β π π¦ β€ ((πΉβπ)βπ€)) |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π₯ = π€ β (βπ β π π¦ β€ ((πΉβπ)βπ€) β βπ β π π¦ β€ ((πΉβπ)βπ€))) |
71 | 60, 70 | bitrd 278 |
. . . . . . . . . . . . 13
β’ (π₯ = π€ β (βπ β π π¦ β€ ((πΉβπ)βπ₯) β βπ β π π¦ β€ ((πΉβπ)βπ€))) |
72 | 71 | rexbidv 3178 |
. . . . . . . . . . . 12
β’ (π₯ = π€ β (βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯) β βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ€))) |
73 | | breq1 5151 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π§ β (π¦ β€ ((πΉβπ)βπ€) β π§ β€ ((πΉβπ)βπ€))) |
74 | 73 | ralbidv 3177 |
. . . . . . . . . . . . . 14
β’ (π¦ = π§ β (βπ β π π¦ β€ ((πΉβπ)βπ€) β βπ β π π§ β€ ((πΉβπ)βπ€))) |
75 | 74 | cbvrexvw 3235 |
. . . . . . . . . . . . 13
β’
(βπ¦ β
β βπ β
π π¦ β€ ((πΉβπ)βπ€) β βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ€)) |
76 | 75 | a1i 11 |
. . . . . . . . . . . 12
β’ (π₯ = π€ β (βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ€) β βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ€))) |
77 | 72, 76 | bitrd 278 |
. . . . . . . . . . 11
β’ (π₯ = π€ β (βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯) β βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ€))) |
78 | 44, 48, 49, 50, 57, 77 | cbvrabcsfw 3937 |
. . . . . . . . . 10
β’ {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)} = {π€ β β©
π β π dom (πΉβπ) β£ βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ€)} |
79 | 16, 78 | eqtri 2760 |
. . . . . . . . 9
β’ π· = {π€ β β©
π β π dom (πΉβπ) β£ βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ€)} |
80 | 43, 79 | elrab2 3686 |
. . . . . . . 8
β’ (π₯ β π· β (π₯ β β©
π β π dom (πΉβπ) β§ βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ₯))) |
81 | 80 | biimpi 215 |
. . . . . . 7
β’ (π₯ β π· β (π₯ β β©
π β π dom (πΉβπ) β§ βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ₯))) |
82 | 81 | simprd 496 |
. . . . . 6
β’ (π₯ β π· β βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ₯)) |
83 | 82 | adantl 482 |
. . . . 5
β’ ((π β§ π₯ β π·) β βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ₯)) |
84 | | renegcl 11525 |
. . . . . . . 8
β’ (π§ β β β -π§ β
β) |
85 | 84 | ad2antlr 725 |
. . . . . . 7
β’ ((((π β§ π₯ β π·) β§ π§ β β) β§ βπ β π π§ β€ ((πΉβπ)βπ₯)) β -π§ β β) |
86 | | fveq2 6891 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΉβπ) = (πΉβπ)) |
87 | 86 | fveq1d 6893 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
88 | 87 | breq2d 5160 |
. . . . . . . . . . . 12
β’ (π = π β (π§ β€ ((πΉβπ)βπ₯) β π§ β€ ((πΉβπ)βπ₯))) |
89 | 88 | rspcva 3610 |
. . . . . . . . . . 11
β’ ((π β π β§ βπ β π π§ β€ ((πΉβπ)βπ₯)) β π§ β€ ((πΉβπ)βπ₯)) |
90 | 89 | ancoms 459 |
. . . . . . . . . 10
β’
((βπ β
π π§ β€ ((πΉβπ)βπ₯) β§ π β π) β π§ β€ ((πΉβπ)βπ₯)) |
91 | 90 | adantll 712 |
. . . . . . . . 9
β’
(((((π β§ π₯ β π·) β§ π§ β β) β§ βπ β π π§ β€ ((πΉβπ)βπ₯)) β§ π β π) β π§ β€ ((πΉβπ)βπ₯)) |
92 | | simpllr 774 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π·) β§ π§ β β) β§ βπ β π π§ β€ ((πΉβπ)βπ₯)) β§ π β π) β π§ β β) |
93 | 25 | ad4ant14 750 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π·) β§ π§ β β) β§ βπ β π π§ β€ ((πΉβπ)βπ₯)) β§ π β π) β ((πΉβπ)βπ₯) β β) |
94 | 92, 93 | lenegd 11795 |
. . . . . . . . 9
β’
(((((π β§ π₯ β π·) β§ π§ β β) β§ βπ β π π§ β€ ((πΉβπ)βπ₯)) β§ π β π) β (π§ β€ ((πΉβπ)βπ₯) β -((πΉβπ)βπ₯) β€ -π§)) |
95 | 91, 94 | mpbid 231 |
. . . . . . . 8
β’
(((((π β§ π₯ β π·) β§ π§ β β) β§ βπ β π π§ β€ ((πΉβπ)βπ₯)) β§ π β π) β -((πΉβπ)βπ₯) β€ -π§) |
96 | 95 | ralrimiva 3146 |
. . . . . . 7
β’ ((((π β§ π₯ β π·) β§ π§ β β) β§ βπ β π π§ β€ ((πΉβπ)βπ₯)) β βπ β π -((πΉβπ)βπ₯) β€ -π§) |
97 | | brralrspcev 5208 |
. . . . . . 7
β’ ((-π§ β β β§
βπ β π -((πΉβπ)βπ₯) β€ -π§) β βπ¦ β β βπ β π -((πΉβπ)βπ₯) β€ π¦) |
98 | 85, 96, 97 | syl2anc 584 |
. . . . . 6
β’ ((((π β§ π₯ β π·) β§ π§ β β) β§ βπ β π π§ β€ ((πΉβπ)βπ₯)) β βπ¦ β β βπ β π -((πΉβπ)βπ₯) β€ π¦) |
99 | 98 | rexlimdva2 3157 |
. . . . 5
β’ ((π β§ π₯ β π·) β (βπ§ β β βπ β π π§ β€ ((πΉβπ)βπ₯) β βπ¦ β β βπ β π -((πΉβπ)βπ₯) β€ π¦)) |
100 | 83, 99 | mpd 15 |
. . . 4
β’ ((π β§ π₯ β π·) β βπ¦ β β βπ β π -((πΉβπ)βπ₯) β€ π¦) |
101 | 3, 7, 39, 100 | suprclrnmpt 44034 |
. . 3
β’ ((π β§ π₯ β π·) β sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < ) β
β) |
102 | 16 | a1i 11 |
. . . . . . 7
β’ (π β π· = {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)}) |
103 | | nfv 1917 |
. . . . . . . . . 10
β’
β²π¦(π β§ π₯ β β©
π β π dom (πΉβπ)) |
104 | | nfv 1917 |
. . . . . . . . . 10
β’
β²π¦βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§ |
105 | | renegcl 11525 |
. . . . . . . . . . . . 13
β’ (π¦ β β β -π¦ β
β) |
106 | 105 | 3ad2ant2 1134 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π¦ β β β§ βπ β π π¦ β€ ((πΉβπ)βπ₯)) β -π¦ β β) |
107 | | nfv 1917 |
. . . . . . . . . . . . . . 15
β’
β²ππ |
108 | | nfcv 2903 |
. . . . . . . . . . . . . . . 16
β’
β²ππ₯ |
109 | | nfii1 5032 |
. . . . . . . . . . . . . . . 16
β’
β²πβ© π β π dom (πΉβπ) |
110 | 108, 109 | nfel 2917 |
. . . . . . . . . . . . . . 15
β’
β²π π₯ β β© π β π dom (πΉβπ) |
111 | 107, 110 | nfan 1902 |
. . . . . . . . . . . . . 14
β’
β²π(π β§ π₯ β β©
π β π dom (πΉβπ)) |
112 | 62 | nfel1 2919 |
. . . . . . . . . . . . . 14
β’
β²π π¦ β β |
113 | | nfra1 3281 |
. . . . . . . . . . . . . 14
β’
β²πβπ β π π¦ β€ ((πΉβπ)βπ₯) |
114 | 111, 112,
113 | nf3an 1904 |
. . . . . . . . . . . . 13
β’
β²π((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π¦ β β β§ βπ β π π¦ β€ ((πΉβπ)βπ₯)) |
115 | | simpl2 1192 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π¦ β β β§ βπ β π π¦ β€ ((πΉβπ)βπ₯)) β§ π β π) β π¦ β β) |
116 | | simpll 765 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π β π) β π) |
117 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π β π) β π β π) |
118 | 22 | adantll 712 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π β π) β π₯ β dom (πΉβπ)) |
119 | 13 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π β§ π₯ β dom (πΉβπ)) β (πΉβπ):dom (πΉβπ)βΆβ) |
120 | | simp3 1138 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π β§ π₯ β dom (πΉβπ)) β π₯ β dom (πΉβπ)) |
121 | 119, 120 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π β§ π₯ β dom (πΉβπ)) β ((πΉβπ)βπ₯) β β) |
122 | 116, 117,
118, 121 | syl3anc 1371 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π β π) β ((πΉβπ)βπ₯) β β) |
123 | 122 | 3ad2antl1 1185 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π¦ β β β§ βπ β π π¦ β€ ((πΉβπ)βπ₯)) β§ π β π) β ((πΉβπ)βπ₯) β β) |
124 | | rspa 3245 |
. . . . . . . . . . . . . . . 16
β’
((βπ β
π π¦ β€ ((πΉβπ)βπ₯) β§ π β π) β π¦ β€ ((πΉβπ)βπ₯)) |
125 | 124 | 3ad2antl3 1187 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π¦ β β β§ βπ β π π¦ β€ ((πΉβπ)βπ₯)) β§ π β π) β π¦ β€ ((πΉβπ)βπ₯)) |
126 | | leneg 11719 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β β β§ ((πΉβπ)βπ₯) β β) β (π¦ β€ ((πΉβπ)βπ₯) β -((πΉβπ)βπ₯) β€ -π¦)) |
127 | 126 | biimp3a 1469 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β β§ ((πΉβπ)βπ₯) β β β§ π¦ β€ ((πΉβπ)βπ₯)) β -((πΉβπ)βπ₯) β€ -π¦) |
128 | 115, 123,
125, 127 | syl3anc 1371 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π¦ β β β§ βπ β π π¦ β€ ((πΉβπ)βπ₯)) β§ π β π) β -((πΉβπ)βπ₯) β€ -π¦) |
129 | 128 | ex 413 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π¦ β β β§ βπ β π π¦ β€ ((πΉβπ)βπ₯)) β (π β π β -((πΉβπ)βπ₯) β€ -π¦)) |
130 | 114, 129 | ralrimi 3254 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π¦ β β β§ βπ β π π¦ β€ ((πΉβπ)βπ₯)) β βπ β π -((πΉβπ)βπ₯) β€ -π¦) |
131 | | brralrspcev 5208 |
. . . . . . . . . . . 12
β’ ((-π¦ β β β§
βπ β π -((πΉβπ)βπ₯) β€ -π¦) β βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§) |
132 | 106, 130,
131 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π¦ β β β§ βπ β π π¦ β€ ((πΉβπ)βπ₯)) β βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§) |
133 | 132 | 3exp 1119 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β©
π β π dom (πΉβπ)) β (π¦ β β β (βπ β π π¦ β€ ((πΉβπ)βπ₯) β βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§))) |
134 | 103, 104,
133 | rexlimd 3263 |
. . . . . . . . 9
β’ ((π β§ π₯ β β©
π β π dom (πΉβπ)) β (βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯) β βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§)) |
135 | 84 | 3ad2ant2 1134 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π§ β β β§ βπ β π -((πΉβπ)βπ₯) β€ π§) β -π§ β β) |
136 | | nfv 1917 |
. . . . . . . . . . . . . 14
β’
β²π π§ β β |
137 | | nfra1 3281 |
. . . . . . . . . . . . . 14
β’
β²πβπ β π -((πΉβπ)βπ₯) β€ π§ |
138 | 111, 136,
137 | nf3an 1904 |
. . . . . . . . . . . . 13
β’
β²π((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π§ β β β§ βπ β π -((πΉβπ)βπ₯) β€ π§) |
139 | 122 | 3ad2antl1 1185 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π§ β β β§ βπ β π -((πΉβπ)βπ₯) β€ π§) β§ π β π) β ((πΉβπ)βπ₯) β β) |
140 | | simpl2 1192 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π§ β β β§ βπ β π -((πΉβπ)βπ₯) β€ π§) β§ π β π) β π§ β β) |
141 | | rspa 3245 |
. . . . . . . . . . . . . . . 16
β’
((βπ β
π -((πΉβπ)βπ₯) β€ π§ β§ π β π) β -((πΉβπ)βπ₯) β€ π§) |
142 | 141 | 3ad2antl3 1187 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π§ β β β§ βπ β π -((πΉβπ)βπ₯) β€ π§) β§ π β π) β -((πΉβπ)βπ₯) β€ π§) |
143 | | simp3 1138 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ)βπ₯) β β β§ π§ β β β§ -((πΉβπ)βπ₯) β€ π§) β -((πΉβπ)βπ₯) β€ π§) |
144 | | renegcl 11525 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΉβπ)βπ₯) β β β -((πΉβπ)βπ₯) β β) |
145 | 144 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ)βπ₯) β β β§ π§ β β) β -((πΉβπ)βπ₯) β β) |
146 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ)βπ₯) β β β§ π§ β β) β π§ β β) |
147 | | leneg 11719 |
. . . . . . . . . . . . . . . . . . 19
β’
((-((πΉβπ)βπ₯) β β β§ π§ β β) β (-((πΉβπ)βπ₯) β€ π§ β -π§ β€ --((πΉβπ)βπ₯))) |
148 | 145, 146,
147 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ)βπ₯) β β β§ π§ β β) β (-((πΉβπ)βπ₯) β€ π§ β -π§ β€ --((πΉβπ)βπ₯))) |
149 | 148 | 3adant3 1132 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ)βπ₯) β β β§ π§ β β β§ -((πΉβπ)βπ₯) β€ π§) β (-((πΉβπ)βπ₯) β€ π§ β -π§ β€ --((πΉβπ)βπ₯))) |
150 | 143, 149 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉβπ)βπ₯) β β β§ π§ β β β§ -((πΉβπ)βπ₯) β€ π§) β -π§ β€ --((πΉβπ)βπ₯)) |
151 | | recn 11202 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉβπ)βπ₯) β β β ((πΉβπ)βπ₯) β β) |
152 | 151 | negnegd 11564 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ)βπ₯) β β β --((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
153 | 152 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉβπ)βπ₯) β β β§ π§ β β β§ -((πΉβπ)βπ₯) β€ π§) β --((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
154 | 150, 153 | breqtrd 5174 |
. . . . . . . . . . . . . . 15
β’ ((((πΉβπ)βπ₯) β β β§ π§ β β β§ -((πΉβπ)βπ₯) β€ π§) β -π§ β€ ((πΉβπ)βπ₯)) |
155 | 139, 140,
142, 154 | syl3anc 1371 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π§ β β β§ βπ β π -((πΉβπ)βπ₯) β€ π§) β§ π β π) β -π§ β€ ((πΉβπ)βπ₯)) |
156 | 155 | ex 413 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π§ β β β§ βπ β π -((πΉβπ)βπ₯) β€ π§) β (π β π β -π§ β€ ((πΉβπ)βπ₯))) |
157 | 138, 156 | ralrimi 3254 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π§ β β β§ βπ β π -((πΉβπ)βπ₯) β€ π§) β βπ β π -π§ β€ ((πΉβπ)βπ₯)) |
158 | | breq1 5151 |
. . . . . . . . . . . . . 14
β’ (π¦ = -π§ β (π¦ β€ ((πΉβπ)βπ₯) β -π§ β€ ((πΉβπ)βπ₯))) |
159 | 158 | ralbidv 3177 |
. . . . . . . . . . . . 13
β’ (π¦ = -π§ β (βπ β π π¦ β€ ((πΉβπ)βπ₯) β βπ β π -π§ β€ ((πΉβπ)βπ₯))) |
160 | 159 | rspcev 3612 |
. . . . . . . . . . . 12
β’ ((-π§ β β β§
βπ β π -π§ β€ ((πΉβπ)βπ₯)) β βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)) |
161 | 135, 157,
160 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β©
π β π dom (πΉβπ)) β§ π§ β β β§ βπ β π -((πΉβπ)βπ₯) β€ π§) β βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)) |
162 | 161 | 3exp 1119 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β©
π β π dom (πΉβπ)) β (π§ β β β (βπ β π -((πΉβπ)βπ₯) β€ π§ β βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)))) |
163 | 162 | rexlimdv 3153 |
. . . . . . . . 9
β’ ((π β§ π₯ β β©
π β π dom (πΉβπ)) β (βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§ β βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯))) |
164 | 134, 163 | impbid 211 |
. . . . . . . 8
β’ ((π β§ π₯ β β©
π β π dom (πΉβπ)) β (βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯) β βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§)) |
165 | 32, 164 | rabbida 3458 |
. . . . . . 7
β’ (π β {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)} = {π₯ β β©
π β π dom (πΉβπ) β£ βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§}) |
166 | 102, 165 | eqtrd 2772 |
. . . . . 6
β’ (π β π· = {π₯ β β©
π β π dom (πΉβπ) β£ βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§}) |
167 | 32, 166 | alrimi 2206 |
. . . . 5
β’ (π β βπ₯ π· = {π₯ β β©
π β π dom (πΉβπ) β£ βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§}) |
168 | | eqid 2732 |
. . . . . . 7
β’ sup(ran
(π β π β¦ -((πΉβπ)βπ₯)), β, < ) = sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < ) |
169 | 168 | rgenw 3065 |
. . . . . 6
β’
βπ₯ β
π· sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < ) = sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < ) |
170 | 169 | a1i 11 |
. . . . 5
β’ (π β βπ₯ β π· sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < ) = sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < )) |
171 | | mpteq12f 5236 |
. . . . 5
β’
((βπ₯ π· = {π₯ β β©
π β π dom (πΉβπ) β£ βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§} β§ βπ₯ β π· sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < ) = sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < )) β (π₯ β π· β¦ sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < )) = (π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§} β¦ sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < ))) |
172 | 167, 170,
171 | syl2anc 584 |
. . . 4
β’ (π β (π₯ β π· β¦ sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < )) = (π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§} β¦ sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < ))) |
173 | | nfv 1917 |
. . . . 5
β’
β²π§π |
174 | 121 | renegcld 11643 |
. . . . 5
β’ ((π β§ π β π β§ π₯ β dom (πΉβπ)) β -((πΉβπ)βπ₯) β β) |
175 | | nfv 1917 |
. . . . . 6
β’
β²π₯(π β§ π β π) |
176 | 34 | a1i 11 |
. . . . . 6
β’ ((π β§ π β π) β dom (πΉβπ) β V) |
177 | 121 | 3expa 1118 |
. . . . . 6
β’ (((π β§ π β π) β§ π₯ β dom (πΉβπ)) β ((πΉβπ)βπ₯) β β) |
178 | 13 | feqmptd 6960 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΉβπ) = (π₯ β dom (πΉβπ) β¦ ((πΉβπ)βπ₯))) |
179 | 178 | eqcomd 2738 |
. . . . . . 7
β’ ((π β§ π β π) β (π₯ β dom (πΉβπ) β¦ ((πΉβπ)βπ₯)) = (πΉβπ)) |
180 | 179, 11 | eqeltrd 2833 |
. . . . . 6
β’ ((π β§ π β π) β (π₯ β dom (πΉβπ) β¦ ((πΉβπ)βπ₯)) β (SMblFnβπ)) |
181 | 175, 9, 176, 177, 180 | smfneg 45598 |
. . . . 5
β’ ((π β§ π β π) β (π₯ β dom (πΉβπ) β¦ -((πΉβπ)βπ₯)) β (SMblFnβπ)) |
182 | | eqid 2732 |
. . . . 5
β’ {π₯ β β© π β π dom (πΉβπ) β£ βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§} = {π₯ β β©
π β π dom (πΉβπ) β£ βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§} |
183 | | eqid 2732 |
. . . . 5
β’ (π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§} β¦ sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < )) = (π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§} β¦ sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < )) |
184 | 107, 32, 173, 4, 5, 8, 174, 181, 182, 183 | smfsupmpt 45610 |
. . . 4
β’ (π β (π₯ β {π₯ β β©
π β π dom (πΉβπ) β£ βπ§ β β βπ β π -((πΉβπ)βπ₯) β€ π§} β¦ sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < )) β
(SMblFnβπ)) |
185 | 172, 184 | eqeltrd 2833 |
. . 3
β’ (π β (π₯ β π· β¦ sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < )) β
(SMblFnβπ)) |
186 | 32, 8, 38, 101, 185 | smfneg 45598 |
. 2
β’ (π β (π₯ β π· β¦ -sup(ran (π β π β¦ -((πΉβπ)βπ₯)), β, < )) β
(SMblFnβπ)) |
187 | 31, 186 | eqeltrd 2833 |
1
β’ (π β πΊ β (SMblFnβπ)) |