Step | Hyp | Ref
| Expression |
1 | | nmoolb.2 |
. . . . . 6
β’ π = (BaseSetβπ) |
2 | | nmoolb.m |
. . . . . 6
β’ π =
(normCVβπ) |
3 | 1, 2 | nmosetre 30522 |
. . . . 5
β’ ((π β NrmCVec β§ π:πβΆπ) β {π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))} β β) |
4 | | ressxr 11259 |
. . . . 5
β’ β
β β* |
5 | 3, 4 | sstrdi 3989 |
. . . 4
β’ ((π β NrmCVec β§ π:πβΆπ) β {π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))} β
β*) |
6 | 5 | 3adant1 1127 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β {π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))} β
β*) |
7 | | fveq2 6884 |
. . . . . . . 8
β’ (π¦ = π΄ β (πΏβπ¦) = (πΏβπ΄)) |
8 | 7 | breq1d 5151 |
. . . . . . 7
β’ (π¦ = π΄ β ((πΏβπ¦) β€ 1 β (πΏβπ΄) β€ 1)) |
9 | | 2fveq3 6889 |
. . . . . . . 8
β’ (π¦ = π΄ β (πβ(πβπ¦)) = (πβ(πβπ΄))) |
10 | 9 | eqeq2d 2737 |
. . . . . . 7
β’ (π¦ = π΄ β ((πβ(πβπ΄)) = (πβ(πβπ¦)) β (πβ(πβπ΄)) = (πβ(πβπ΄)))) |
11 | 8, 10 | anbi12d 630 |
. . . . . 6
β’ (π¦ = π΄ β (((πΏβπ¦) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ¦))) β ((πΏβπ΄) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ΄))))) |
12 | | eqid 2726 |
. . . . . . 7
β’ (πβ(πβπ΄)) = (πβ(πβπ΄)) |
13 | 12 | biantru 529 |
. . . . . 6
β’ ((πΏβπ΄) β€ 1 β ((πΏβπ΄) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ΄)))) |
14 | 11, 13 | bitr4di 289 |
. . . . 5
β’ (π¦ = π΄ β (((πΏβπ¦) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ¦))) β (πΏβπ΄) β€ 1)) |
15 | 14 | rspcev 3606 |
. . . 4
β’ ((π΄ β π β§ (πΏβπ΄) β€ 1) β βπ¦ β π ((πΏβπ¦) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ¦)))) |
16 | | fvex 6897 |
. . . . 5
β’ (πβ(πβπ΄)) β V |
17 | | eqeq1 2730 |
. . . . . . 7
β’ (π₯ = (πβ(πβπ΄)) β (π₯ = (πβ(πβπ¦)) β (πβ(πβπ΄)) = (πβ(πβπ¦)))) |
18 | 17 | anbi2d 628 |
. . . . . 6
β’ (π₯ = (πβ(πβπ΄)) β (((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦))) β ((πΏβπ¦) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ¦))))) |
19 | 18 | rexbidv 3172 |
. . . . 5
β’ (π₯ = (πβ(πβπ΄)) β (βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦))) β βπ¦ β π ((πΏβπ¦) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ¦))))) |
20 | 16, 19 | elab 3663 |
. . . 4
β’ ((πβ(πβπ΄)) β {π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))} β βπ¦ β π ((πΏβπ¦) β€ 1 β§ (πβ(πβπ΄)) = (πβ(πβπ¦)))) |
21 | 15, 20 | sylibr 233 |
. . 3
β’ ((π΄ β π β§ (πΏβπ΄) β€ 1) β (πβ(πβπ΄)) β {π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))}) |
22 | | supxrub 13306 |
. . 3
β’ (({π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))} β β* β§ (πβ(πβπ΄)) β {π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))}) β (πβ(πβπ΄)) β€ sup({π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))}, β*, <
)) |
23 | 6, 21, 22 | syl2an 595 |
. 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 30521 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β (πβπ) = sup({π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))}, β*, <
)) |
28 | 27 | adantr 480 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β§ (π΄ β π β§ (πΏβπ΄) β€ 1)) β (πβπ) = sup({π₯ β£ βπ¦ β π ((πΏβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))}, β*, <
)) |
29 | 23, 28 | breqtrrd 5169 |
1
β’ (((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β§ (π΄ β π β§ (πΏβπ΄) β€ 1)) β (πβ(πβπ΄)) β€ (πβπ)) |