Step | Hyp | Ref
| Expression |
1 | | nmfnval 31623 |
. . . 4
β’ (π: ββΆβ β
(normfnβπ)
= sup({π¦ β£
βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}, β*, <
)) |
2 | 1 | adantr 480 |
. . 3
β’ ((π: ββΆβ β§
π΄ β
β*) β (normfnβπ) = sup({π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}, β*, <
)) |
3 | 2 | breq1d 5149 |
. 2
β’ ((π: ββΆβ β§
π΄ β
β*) β ((normfnβπ) β€ π΄ β sup({π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}, β*, < ) β€ π΄)) |
4 | | nmfnsetre 31624 |
. . . . 5
β’ (π: ββΆβ β
{π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))} β β) |
5 | | ressxr 11257 |
. . . . 5
β’ β
β β* |
6 | 4, 5 | sstrdi 3987 |
. . . 4
β’ (π: ββΆβ β
{π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))} β
β*) |
7 | | supxrleub 13306 |
. . . 4
β’ (({π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))} β β* β§ π΄ β β*)
β (sup({π¦ β£
βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}, β*, < ) β€ π΄ β βπ§ β {π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}π§ β€ π΄)) |
8 | 6, 7 | sylan 579 |
. . 3
β’ ((π: ββΆβ β§
π΄ β
β*) β (sup({π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}, β*, < ) β€ π΄ β βπ§ β {π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}π§ β€ π΄)) |
9 | | ancom 460 |
. . . . . . 7
β’
(((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯))) β (π¦ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1)) |
10 | | eqeq1 2728 |
. . . . . . . 8
β’ (π¦ = π§ β (π¦ = (absβ(πβπ₯)) β π§ = (absβ(πβπ₯)))) |
11 | 10 | anbi1d 629 |
. . . . . . 7
β’ (π¦ = π§ β ((π¦ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β (π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1))) |
12 | 9, 11 | bitrid 283 |
. . . . . 6
β’ (π¦ = π§ β
(((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯))) β (π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1))) |
13 | 12 | rexbidv 3170 |
. . . . 5
β’ (π¦ = π§ β (βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯))) β βπ₯ β β (π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1))) |
14 | 13 | ralab 3680 |
. . . 4
β’
(βπ§ β
{π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}π§ β€ π΄ β βπ§(βπ₯ β β (π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄)) |
15 | | ralcom4 3275 |
. . . . 5
β’
(βπ₯ β
β βπ§((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄) β βπ§βπ₯ β β ((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄)) |
16 | | impexp 450 |
. . . . . . . 8
β’ (((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄) β (π§ = (absβ(πβπ₯)) β
((normββπ₯) β€ 1 β π§ β€ π΄))) |
17 | 16 | albii 1813 |
. . . . . . 7
β’
(βπ§((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄) β βπ§(π§ = (absβ(πβπ₯)) β
((normββπ₯) β€ 1 β π§ β€ π΄))) |
18 | | fvex 6895 |
. . . . . . . 8
β’
(absβ(πβπ₯)) β V |
19 | | breq1 5142 |
. . . . . . . . 9
β’ (π§ = (absβ(πβπ₯)) β (π§ β€ π΄ β (absβ(πβπ₯)) β€ π΄)) |
20 | 19 | imbi2d 340 |
. . . . . . . 8
β’ (π§ = (absβ(πβπ₯)) β
(((normββπ₯) β€ 1 β π§ β€ π΄) β
((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄))) |
21 | 18, 20 | ceqsalv 3504 |
. . . . . . 7
β’
(βπ§(π§ = (absβ(πβπ₯)) β
((normββπ₯) β€ 1 β π§ β€ π΄)) β
((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄)) |
22 | 17, 21 | bitri 275 |
. . . . . 6
β’
(βπ§((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄) β
((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄)) |
23 | 22 | ralbii 3085 |
. . . . 5
β’
(βπ₯ β
β βπ§((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄) β βπ₯ β β
((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄)) |
24 | | r19.23v 3174 |
. . . . . 6
β’
(βπ₯ β
β ((π§ =
(absβ(πβπ₯)) β§
(normββπ₯) β€ 1) β π§ β€ π΄) β (βπ₯ β β (π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄)) |
25 | 24 | albii 1813 |
. . . . 5
β’
(βπ§βπ₯ β β ((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄) β βπ§(βπ₯ β β (π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄)) |
26 | 15, 23, 25 | 3bitr3i 301 |
. . . 4
β’
(βπ₯ β
β ((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄) β βπ§(βπ₯ β β (π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄)) |
27 | 14, 26 | bitr4i 278 |
. . 3
β’
(βπ§ β
{π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}π§ β€ π΄ β βπ₯ β β
((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄)) |
28 | 8, 27 | bitrdi 287 |
. 2
β’ ((π: ββΆβ β§
π΄ β
β*) β (sup({π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}, β*, < ) β€ π΄ β βπ₯ β β
((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄))) |
29 | 3, 28 | bitrd 279 |
1
β’ ((π: ββΆβ β§
π΄ β
β*) β ((normfnβπ) β€ π΄ β βπ₯ β β
((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄))) |