Step | Hyp | Ref
| Expression |
1 | | nmfnval 30867 |
. . . 4
β’ (π: ββΆβ β
(normfnβπ)
= sup({π¦ β£
βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}, β*, <
)) |
2 | 1 | adantr 482 |
. . 3
β’ ((π: ββΆβ β§
π΄ β
β*) β (normfnβπ) = sup({π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}, β*, <
)) |
3 | 2 | breq1d 5119 |
. 2
β’ ((π: ββΆβ β§
π΄ β
β*) β ((normfnβπ) β€ π΄ β sup({π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}, β*, < ) β€ π΄)) |
4 | | nmfnsetre 30868 |
. . . . 5
β’ (π: ββΆβ β
{π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))} β β) |
5 | | ressxr 11207 |
. . . . 5
β’ β
β β* |
6 | 4, 5 | sstrdi 3960 |
. . . 4
β’ (π: ββΆβ β
{π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))} β
β*) |
7 | | supxrleub 13254 |
. . . 4
β’ (({π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))} β β* β§ π΄ β β*)
β (sup({π¦ β£
βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}, β*, < ) β€ π΄ β βπ§ β {π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}π§ β€ π΄)) |
8 | 6, 7 | sylan 581 |
. . 3
β’ ((π: ββΆβ β§
π΄ β
β*) β (sup({π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}, β*, < ) β€ π΄ β βπ§ β {π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}π§ β€ π΄)) |
9 | | ancom 462 |
. . . . . . 7
β’
(((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯))) β (π¦ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1)) |
10 | | eqeq1 2737 |
. . . . . . . 8
β’ (π¦ = π§ β (π¦ = (absβ(πβπ₯)) β π§ = (absβ(πβπ₯)))) |
11 | 10 | anbi1d 631 |
. . . . . . 7
β’ (π¦ = π§ β ((π¦ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β (π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1))) |
12 | 9, 11 | bitrid 283 |
. . . . . 6
β’ (π¦ = π§ β
(((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯))) β (π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1))) |
13 | 12 | rexbidv 3172 |
. . . . 5
β’ (π¦ = π§ β (βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯))) β βπ₯ β β (π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1))) |
14 | 13 | ralab 3653 |
. . . 4
β’
(βπ§ β
{π¦ β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π¦ = (absβ(πβπ₯)))}π§ β€ π΄ β βπ§(βπ₯ β β (π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄)) |
15 | | ralcom4 3268 |
. . . . 5
β’
(βπ₯ β
β βπ§((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄) β βπ§βπ₯ β β ((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄)) |
16 | | impexp 452 |
. . . . . . . 8
β’ (((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄) β (π§ = (absβ(πβπ₯)) β
((normββπ₯) β€ 1 β π§ β€ π΄))) |
17 | 16 | albii 1822 |
. . . . . . 7
β’
(βπ§((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄) β βπ§(π§ = (absβ(πβπ₯)) β
((normββπ₯) β€ 1 β π§ β€ π΄))) |
18 | | fvex 6859 |
. . . . . . . 8
β’
(absβ(πβπ₯)) β V |
19 | | breq1 5112 |
. . . . . . . . 9
β’ (π§ = (absβ(πβπ₯)) β (π§ β€ π΄ β (absβ(πβπ₯)) β€ π΄)) |
20 | 19 | imbi2d 341 |
. . . . . . . 8
β’ (π§ = (absβ(πβπ₯)) β
(((normββπ₯) β€ 1 β π§ β€ π΄) β
((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄))) |
21 | 18, 20 | ceqsalv 3483 |
. . . . . . 7
β’
(βπ§(π§ = (absβ(πβπ₯)) β
((normββπ₯) β€ 1 β π§ β€ π΄)) β
((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄)) |
22 | 17, 21 | bitri 275 |
. . . . . 6
β’
(βπ§((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄) β
((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄)) |
23 | 22 | ralbii 3093 |
. . . . 5
β’
(βπ₯ β
β βπ§((π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄) β βπ₯ β β
((normββπ₯) β€ 1 β (absβ(πβπ₯)) β€ π΄)) |
24 | | r19.23v 3176 |
. . . . . 6
β’
(βπ₯ β
β ((π§ =
(absβ(πβπ₯)) β§
(normββπ₯) β€ 1) β π§ β€ π΄) β (βπ₯ β β (π§ = (absβ(πβπ₯)) β§ (normββπ₯) β€ 1) β π§ β€ π΄)) |
25 | 24 | albii 1822 |
. . . . 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β(πβπ₯)) β€ π΄))) |