Step | Hyp | Ref
| Expression |
1 | | nmoolb.2 |
. . . . . 6
β’ π = (BaseSetβπ) |
2 | | nmoolb.m |
. . . . . 6
β’ π =
(normCVβπ) |
3 | 1, 2 | nmosetre 29748 |
. . . . 5
β’ ((π β NrmCVec β§ π:πβΆπ) β {π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))} β β) |
4 | | ressxr 11204 |
. . . . 5
β’ β
β β* |
5 | 3, 4 | sstrdi 3957 |
. . . 4
β’ ((π β NrmCVec β§ π:πβΆπ) β {π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))} β
β*) |
6 | 5 | 3adant1 1131 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β {π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))} β
β*) |
7 | | fveq2 6843 |
. . . . . . . 8
β’ (π¦ = π΄ β (πΏβπ¦) = (πΏβπ΄)) |
8 | 7 | breq1d 5116 |
. . . . . . 7
β’ (π¦ = π΄ β ((πΏβπ¦) β€ 1 β (πΏβπ΄) β€ 1)) |
9 | | 2fveq3 6848 |
. . . . . . . 8
β’ (π¦ = π΄ β (πβ(πβπ¦)) = (πβ(πβπ΄))) |
10 | 9 | eqeq2d 2744 |
. . . . . . 7
β’ (π¦ = π΄ β ((πβ(πβπ΄)) = (πβ(πβπ¦)) β (πβ(πβπ΄)) = (πβ(πβπ΄)))) |
11 | 8, 10 | anbi12d 632 |
. . . . . 6
β’ (π¦ = π΄ β (((πΏβπ¦) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ¦))) β ((πΏβπ΄) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ΄))))) |
12 | | eqid 2733 |
. . . . . . 7
β’ (πβ(πβπ΄)) = (πβ(πβπ΄)) |
13 | 12 | biantru 531 |
. . . . . 6
β’ ((πΏβπ΄) β€ 1 β ((πΏβπ΄) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ΄)))) |
14 | 11, 13 | bitr4di 289 |
. . . . 5
β’ (π¦ = π΄ β (((πΏβπ¦) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ¦))) β (πΏβπ΄) β€ 1)) |
15 | 14 | rspcev 3580 |
. . . 4
β’ ((π΄ β π β§ (πΏβπ΄) β€ 1) β βπ¦ β π ((πΏβπ¦) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ¦)))) |
16 | | fvex 6856 |
. . . . 5
β’ (πβ(πβπ΄)) β V |
17 | | eqeq1 2737 |
. . . . . . 7
β’ (π₯ = (πβ(πβπ΄)) β (π₯ = (πβ(πβπ¦)) β (πβ(πβπ΄)) = (πβ(πβπ¦)))) |
18 | 17 | anbi2d 630 |
. . . . . 6
β’ (π₯ = (πβ(πβπ΄)) β (((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦))) β ((πΏβπ¦) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ¦))))) |
19 | 18 | rexbidv 3172 |
. . . . 5
β’ (π₯ = (πβ(πβπ΄)) β (βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦))) β βπ¦ β π ((πΏβπ¦) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ¦))))) |
20 | 16, 19 | elab 3631 |
. . . 4
β’ ((πβ(πβπ΄)) β {π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))} β βπ¦ β π ((πΏβπ¦) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ¦)))) |
21 | 15, 20 | sylibr 233 |
. . 3
β’ ((π΄ β π β§ (πΏβπ΄) β€ 1) β (πβ(πβπ΄)) β {π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))}) |
22 | | supxrub 13249 |
. . 3
β’ (({π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))} β β* β§ (πβ(πβπ΄)) β {π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))}) β (πβ(πβπ΄)) β€ sup({π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))}, β*, <
)) |
23 | 6, 21, 22 | syl2an 597 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β§ (π΄ β π β§ (πΏβπ΄) β€ 1)) β (πβ(πβπ΄)) β€ sup({π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))}, β*, <
)) |
24 | | nmoolb.1 |
. . . 4
β’ π = (BaseSetβπ) |
25 | | nmoolb.l |
. . . 4
β’ πΏ =
(normCVβπ) |
26 | | nmoolb.3 |
. . . 4
β’ π = (π normOpOLD π) |
27 | 24, 1, 25, 2, 26 | nmooval 29747 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β (πβπ) = sup({π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))}, β*, <
)) |
28 | 27 | adantr 482 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β§ (π΄ β π β§ (πΏβπ΄) β€ 1)) β (πβπ) = sup({π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))}, β*, <
)) |
29 | 23, 28 | breqtrrd 5134 |
1
β’ (((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β§ (π΄ β π β§ (πΏβπ΄) β€ 1)) β (πβ(πβπ΄)) β€ (πβπ)) |