Step | Hyp | Ref
| Expression |
1 | | mbfinf.2 |
. . 3
β’ πΊ = (π₯ β π΄ β¦ inf(ran (π β π β¦ π΅), β, < )) |
2 | | mbfinf.5 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β β) |
3 | 2 | anass1rs 654 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β π) β π΅ β β) |
4 | 3 | fmpttd 7068 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅):πβΆβ) |
5 | 4 | frnd 6681 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β ran (π β π β¦ π΅) β β) |
6 | | mbfinf.3 |
. . . . . . . . . . . 12
β’ (π β π β β€) |
7 | | uzid 12785 |
. . . . . . . . . . . 12
β’ (π β β€ β π β
(β€β₯βπ)) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β (β€β₯βπ)) |
9 | | mbfinf.1 |
. . . . . . . . . . 11
β’ π =
(β€β₯βπ) |
10 | 8, 9 | eleqtrrdi 2849 |
. . . . . . . . . 10
β’ (π β π β π) |
11 | 10 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β π β π) |
12 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β π β¦ π΅) = (π β π β¦ π΅) |
13 | 12, 3 | dmmptd 6651 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β dom (π β π β¦ π΅) = π) |
14 | 11, 13 | eleqtrrd 2841 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β π β dom (π β π β¦ π΅)) |
15 | 14 | ne0d 4300 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β dom (π β π β¦ π΅) β β
) |
16 | | dm0rn0 5885 |
. . . . . . . 8
β’ (dom
(π β π β¦ π΅) = β
β ran (π β π β¦ π΅) = β
) |
17 | 16 | necon3bii 2997 |
. . . . . . 7
β’ (dom
(π β π β¦ π΅) β β
β ran (π β π β¦ π΅) β β
) |
18 | 15, 17 | sylib 217 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β ran (π β π β¦ π΅) β β
) |
19 | | mbfinf.6 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β βπ¦ β β βπ β π π¦ β€ π΅) |
20 | 4 | ffnd 6674 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅) Fn π) |
21 | | breq2 5114 |
. . . . . . . . . . 11
β’ (π§ = ((π β π β¦ π΅)βπ) β (π¦ β€ π§ β π¦ β€ ((π β π β¦ π΅)βπ))) |
22 | 21 | ralrn 7043 |
. . . . . . . . . 10
β’ ((π β π β¦ π΅) Fn π β (βπ§ β ran (π β π β¦ π΅)π¦ β€ π§ β βπ β π π¦ β€ ((π β π β¦ π΅)βπ))) |
23 | 20, 22 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (βπ§ β ran (π β π β¦ π΅)π¦ β€ π§ β βπ β π π¦ β€ ((π β π β¦ π΅)βπ))) |
24 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²ππ¦ |
25 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π
β€ |
26 | | nffvmpt1 6858 |
. . . . . . . . . . . 12
β’
β²π((π β π β¦ π΅)βπ) |
27 | 24, 25, 26 | nfbr 5157 |
. . . . . . . . . . 11
β’
β²π π¦ β€ ((π β π β¦ π΅)βπ) |
28 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π π¦ β€ ((π β π β¦ π΅)βπ) |
29 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΅)βπ)) |
30 | 29 | breq2d 5122 |
. . . . . . . . . . 11
β’ (π = π β (π¦ β€ ((π β π β¦ π΅)βπ) β π¦ β€ ((π β π β¦ π΅)βπ))) |
31 | 27, 28, 30 | cbvralw 3292 |
. . . . . . . . . 10
β’
(βπ β
π π¦ β€ ((π β π β¦ π΅)βπ) β βπ β π π¦ β€ ((π β π β¦ π΅)βπ)) |
32 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π΄) β§ π β π) β π β π) |
33 | 12 | fvmpt2 6964 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π΅ β β) β ((π β π β¦ π΅)βπ) = π΅) |
34 | 32, 3, 33 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π΄) β§ π β π) β ((π β π β¦ π΅)βπ) = π΅) |
35 | 34 | breq2d 5122 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π΄) β§ π β π) β (π¦ β€ ((π β π β¦ π΅)βπ) β π¦ β€ π΅)) |
36 | 35 | ralbidva 3173 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (βπ β π π¦ β€ ((π β π β¦ π΅)βπ) β βπ β π π¦ β€ π΅)) |
37 | 31, 36 | bitrid 283 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (βπ β π π¦ β€ ((π β π β¦ π΅)βπ) β βπ β π π¦ β€ π΅)) |
38 | 23, 37 | bitrd 279 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (βπ§ β ran (π β π β¦ π΅)π¦ β€ π§ β βπ β π π¦ β€ π΅)) |
39 | 38 | rexbidv 3176 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (βπ¦ β β βπ§ β ran (π β π β¦ π΅)π¦ β€ π§ β βπ¦ β β βπ β π π¦ β€ π΅)) |
40 | 19, 39 | mpbird 257 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β βπ¦ β β βπ§ β ran (π β π β¦ π΅)π¦ β€ π§) |
41 | | infrenegsup 12145 |
. . . . . 6
β’ ((ran
(π β π β¦ π΅) β β β§ ran (π β π β¦ π΅) β β
β§ βπ¦ β β βπ§ β ran (π β π β¦ π΅)π¦ β€ π§) β inf(ran (π β π β¦ π΅), β, < ) = -sup({π β β β£ -π β ran (π β π β¦ π΅)}, β, < )) |
42 | 5, 18, 40, 41 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π₯ β π΄) β inf(ran (π β π β¦ π΅), β, < ) = -sup({π β β β£ -π β ran (π β π β¦ π΅)}, β, < )) |
43 | | rabid 3430 |
. . . . . . . . . 10
β’ (π β {π β β β£ -π β ran (π β π β¦ π΅)} β (π β β β§ -π β ran (π β π β¦ π΅))) |
44 | 3 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β π΄) β§ π β π) β π΅ β β) |
45 | 44 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β π΄) β§ π β β) β§ π β π) β π΅ β β) |
46 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ β π΄) β§ π β β) β§ π β π) β π β β) |
47 | 46 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β π΄) β§ π β β) β§ π β π) β π β β) |
48 | | negcon2 11461 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΅ β β β§ π β β) β (π΅ = -π β π = -π΅)) |
49 | 45, 47, 48 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β π΄) β§ π β β) β§ π β π) β (π΅ = -π β π = -π΅)) |
50 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = -π΅ β -π΅ = π) |
51 | 49, 50 | bitrdi 287 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β π΄) β§ π β β) β§ π β π) β (π΅ = -π β -π΅ = π)) |
52 | 34 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β π΄) β§ π β β) β§ π β π) β ((π β π β¦ π΅)βπ) = π΅) |
53 | 52 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β π΄) β§ π β β) β§ π β π) β (((π β π β¦ π΅)βπ) = -π β π΅ = -π)) |
54 | | negex 11406 |
. . . . . . . . . . . . . . . . . . . . 21
β’ -π΅ β V |
55 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β¦ -π΅) = (π β π β¦ -π΅) |
56 | 55 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β π β§ -π΅ β V) β ((π β π β¦ -π΅)βπ) = -π΅) |
57 | 54, 56 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β ((π β π β¦ -π΅)βπ) = -π΅) |
58 | 57 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β π΄) β§ π β β) β§ π β π) β ((π β π β¦ -π΅)βπ) = -π΅) |
59 | 58 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β π΄) β§ π β β) β§ π β π) β (((π β π β¦ -π΅)βπ) = π β -π΅ = π)) |
60 | 51, 53, 59 | 3bitr4d 311 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β π΄) β§ π β β) β§ π β π) β (((π β π β¦ π΅)βπ) = -π β ((π β π β¦ -π΅)βπ) = π)) |
61 | 60 | ralrimiva 3144 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π΄) β§ π β β) β βπ β π (((π β π β¦ π΅)βπ) = -π β ((π β π β¦ -π΅)βπ) = π)) |
62 | 26 | nfeq1 2923 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((π β π β¦ π΅)βπ) = -π |
63 | | nffvmpt1 6858 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π((π β π β¦ -π΅)βπ) |
64 | 63 | nfeq1 2923 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((π β π β¦ -π΅)βπ) = π |
65 | 62, 64 | nfbi 1907 |
. . . . . . . . . . . . . . . . 17
β’
β²π(((π β π β¦ π΅)βπ) = -π β ((π β π β¦ -π΅)βπ) = π) |
66 | | nfv 1918 |
. . . . . . . . . . . . . . . . 17
β’
β²π(((π β π β¦ π΅)βπ) = -π β ((π β π β¦ -π΅)βπ) = π) |
67 | | fveqeq2 6856 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((π β π β¦ π΅)βπ) = -π β ((π β π β¦ π΅)βπ) = -π)) |
68 | | fveqeq2 6856 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((π β π β¦ -π΅)βπ) = π β ((π β π β¦ -π΅)βπ) = π)) |
69 | 67, 68 | bibi12d 346 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((((π β π β¦ π΅)βπ) = -π β ((π β π β¦ -π΅)βπ) = π) β (((π β π β¦ π΅)βπ) = -π β ((π β π β¦ -π΅)βπ) = π))) |
70 | 65, 66, 69 | cbvralw 3292 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
π (((π β π β¦ π΅)βπ) = -π β ((π β π β¦ -π΅)βπ) = π) β βπ β π (((π β π β¦ π΅)βπ) = -π β ((π β π β¦ -π΅)βπ) = π)) |
71 | 61, 70 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΄) β§ π β β) β βπ β π (((π β π β¦ π΅)βπ) = -π β ((π β π β¦ -π΅)βπ) = π)) |
72 | 71 | r19.21bi 3237 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π΄) β§ π β β) β§ π β π) β (((π β π β¦ π΅)βπ) = -π β ((π β π β¦ -π΅)βπ) = π)) |
73 | 72 | rexbidva 3174 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π΄) β§ π β β) β (βπ β π ((π β π β¦ π΅)βπ) = -π β βπ β π ((π β π β¦ -π΅)βπ) = π)) |
74 | 20 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π΄) β§ π β β) β (π β π β¦ π΅) Fn π) |
75 | | fvelrnb 6908 |
. . . . . . . . . . . . . 14
β’ ((π β π β¦ π΅) Fn π β (-π β ran (π β π β¦ π΅) β βπ β π ((π β π β¦ π΅)βπ) = -π)) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π΄) β§ π β β) β (-π β ran (π β π β¦ π΅) β βπ β π ((π β π β¦ π΅)βπ) = -π)) |
77 | 3 | renegcld 11589 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β π΄) β§ π β π) β -π΅ β β) |
78 | 77 | fmpttd 7068 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π΄) β (π β π β¦ -π΅):πβΆβ) |
79 | 78 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΄) β§ π β β) β (π β π β¦ -π΅):πβΆβ) |
80 | 79 | ffnd 6674 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π΄) β§ π β β) β (π β π β¦ -π΅) Fn π) |
81 | | fvelrnb 6908 |
. . . . . . . . . . . . . 14
β’ ((π β π β¦ -π΅) Fn π β (π β ran (π β π β¦ -π΅) β βπ β π ((π β π β¦ -π΅)βπ) = π)) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π΄) β§ π β β) β (π β ran (π β π β¦ -π΅) β βπ β π ((π β π β¦ -π΅)βπ) = π)) |
83 | 73, 76, 82 | 3bitr4d 311 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π΄) β§ π β β) β (-π β ran (π β π β¦ π΅) β π β ran (π β π β¦ -π΅))) |
84 | 83 | pm5.32da 580 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β ((π β β β§ -π β ran (π β π β¦ π΅)) β (π β β β§ π β ran (π β π β¦ -π΅)))) |
85 | 78 | frnd 6681 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β ran (π β π β¦ -π΅) β β) |
86 | 85 | sseld 3948 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (π β ran (π β π β¦ -π΅) β π β β)) |
87 | 86 | pm4.71rd 564 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (π β ran (π β π β¦ -π΅) β (π β β β§ π β ran (π β π β¦ -π΅)))) |
88 | 84, 87 | bitr4d 282 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β ((π β β β§ -π β ran (π β π β¦ π΅)) β π β ran (π β π β¦ -π΅))) |
89 | 43, 88 | bitrid 283 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (π β {π β β β£ -π β ran (π β π β¦ π΅)} β π β ran (π β π β¦ -π΅))) |
90 | 89 | alrimiv 1931 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β βπ(π β {π β β β£ -π β ran (π β π β¦ π΅)} β π β ran (π β π β¦ -π΅))) |
91 | | nfrab1 3429 |
. . . . . . . . 9
β’
β²π{π β β β£ -π β ran (π β π β¦ π΅)} |
92 | | nfcv 2908 |
. . . . . . . . 9
β’
β²πran
(π β π β¦ -π΅) |
93 | 91, 92 | cleqf 2939 |
. . . . . . . 8
β’ ({π β β β£ -π β ran (π β π β¦ π΅)} = ran (π β π β¦ -π΅) β βπ(π β {π β β β£ -π β ran (π β π β¦ π΅)} β π β ran (π β π β¦ -π΅))) |
94 | 90, 93 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β {π β β β£ -π β ran (π β π β¦ π΅)} = ran (π β π β¦ -π΅)) |
95 | 94 | supeq1d 9389 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β sup({π β β β£ -π β ran (π β π β¦ π΅)}, β, < ) = sup(ran (π β π β¦ -π΅), β, < )) |
96 | 95 | negeqd 11402 |
. . . . 5
β’ ((π β§ π₯ β π΄) β -sup({π β β β£ -π β ran (π β π β¦ π΅)}, β, < ) = -sup(ran (π β π β¦ -π΅), β, < )) |
97 | 42, 96 | eqtrd 2777 |
. . . 4
β’ ((π β§ π₯ β π΄) β inf(ran (π β π β¦ π΅), β, < ) = -sup(ran (π β π β¦ -π΅), β, < )) |
98 | 97 | mpteq2dva 5210 |
. . 3
β’ (π β (π₯ β π΄ β¦ inf(ran (π β π β¦ π΅), β, < )) = (π₯ β π΄ β¦ -sup(ran (π β π β¦ -π΅), β, < ))) |
99 | 1, 98 | eqtrid 2789 |
. 2
β’ (π β πΊ = (π₯ β π΄ β¦ -sup(ran (π β π β¦ -π΅), β, < ))) |
100 | | ltso 11242 |
. . . . 5
β’ < Or
β |
101 | 100 | supex 9406 |
. . . 4
β’ sup(ran
(π β π β¦ -π΅), β, < ) β V |
102 | 101 | a1i 11 |
. . 3
β’ ((π β§ π₯ β π΄) β sup(ran (π β π β¦ -π΅), β, < ) β
V) |
103 | | eqid 2737 |
. . . 4
β’ (π₯ β π΄ β¦ sup(ran (π β π β¦ -π΅), β, < )) = (π₯ β π΄ β¦ sup(ran (π β π β¦ -π΅), β, < )) |
104 | 2 | anassrs 469 |
. . . . 5
β’ (((π β§ π β π) β§ π₯ β π΄) β π΅ β β) |
105 | | mbfinf.4 |
. . . . 5
β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) |
106 | 104, 105 | mbfneg 25030 |
. . . 4
β’ ((π β§ π β π) β (π₯ β π΄ β¦ -π΅) β MblFn) |
107 | 2 | renegcld 11589 |
. . . 4
β’ ((π β§ (π β π β§ π₯ β π΄)) β -π΅ β β) |
108 | | renegcl 11471 |
. . . . . . 7
β’ (π¦ β β β -π¦ β
β) |
109 | 108 | ad2antrl 727 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (π¦ β β β§ βπ β π π¦ β€ π΅)) β -π¦ β β) |
110 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π΄) β§ π¦ β β) β§ π β π) β π¦ β β) |
111 | 3 | adantlr 714 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π΄) β§ π¦ β β) β§ π β π) β π΅ β β) |
112 | 110, 111 | lenegd 11741 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π΄) β§ π¦ β β) β§ π β π) β (π¦ β€ π΅ β -π΅ β€ -π¦)) |
113 | 112 | ralbidva 3173 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π¦ β β) β (βπ β π π¦ β€ π΅ β βπ β π -π΅ β€ -π¦)) |
114 | 113 | biimpd 228 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π¦ β β) β (βπ β π π¦ β€ π΅ β βπ β π -π΅ β€ -π¦)) |
115 | 114 | impr 456 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ (π¦ β β β§ βπ β π π¦ β€ π΅)) β βπ β π -π΅ β€ -π¦) |
116 | | brralrspcev 5170 |
. . . . . 6
β’ ((-π¦ β β β§
βπ β π -π΅ β€ -π¦) β βπ§ β β βπ β π -π΅ β€ π§) |
117 | 109, 115,
116 | syl2anc 585 |
. . . . 5
β’ (((π β§ π₯ β π΄) β§ (π¦ β β β§ βπ β π π¦ β€ π΅)) β βπ§ β β βπ β π -π΅ β€ π§) |
118 | 19, 117 | rexlimddv 3159 |
. . . 4
β’ ((π β§ π₯ β π΄) β βπ§ β β βπ β π -π΅ β€ π§) |
119 | 9, 103, 6, 106, 107, 118 | mbfsup 25044 |
. . 3
β’ (π β (π₯ β π΄ β¦ sup(ran (π β π β¦ -π΅), β, < )) β
MblFn) |
120 | 102, 119 | mbfneg 25030 |
. 2
β’ (π β (π₯ β π΄ β¦ -sup(ran (π β π β¦ -π΅), β, < )) β
MblFn) |
121 | 99, 120 | eqeltrd 2838 |
1
β’ (π β πΊ β MblFn) |