Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(BaseSetβπ) =
(BaseSetβπ) |
2 | | eqid 2733 |
. . . . 5
β’
(BaseSetβπ) =
(BaseSetβπ) |
3 | | nmoo0.0 |
. . . . 5
β’ π = (π 0op π) |
4 | 1, 2, 3 | 0oo 30042 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec) β π:(BaseSetβπ)βΆ(BaseSetβπ)) |
5 | | eqid 2733 |
. . . . 5
β’
(normCVβπ) = (normCVβπ) |
6 | | eqid 2733 |
. . . . 5
β’
(normCVβπ) = (normCVβπ) |
7 | | nmoo0.3 |
. . . . 5
β’ π = (π normOpOLD π) |
8 | 1, 2, 5, 6, 7 | nmooval 30016 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:(BaseSetβπ)βΆ(BaseSetβπ)) β (πβπ) = sup({π₯ β£ βπ§ β (BaseSetβπ)(((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))}, β*, <
)) |
9 | 4, 8 | mpd3an3 1463 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec) β (πβπ) = sup({π₯ β£ βπ§ β (BaseSetβπ)(((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))}, β*, <
)) |
10 | | df-sn 4630 |
. . . . 5
β’ {0} =
{π₯ β£ π₯ = 0} |
11 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0vecβπ) = (0vecβπ) |
12 | 1, 11 | nvzcl 29887 |
. . . . . . . . . 10
β’ (π β NrmCVec β
(0vecβπ)
β (BaseSetβπ)) |
13 | 11, 5 | nvz0 29921 |
. . . . . . . . . . 11
β’ (π β NrmCVec β
((normCVβπ)β(0vecβπ)) = 0) |
14 | | 0le1 11737 |
. . . . . . . . . . 11
β’ 0 β€
1 |
15 | 13, 14 | eqbrtrdi 5188 |
. . . . . . . . . 10
β’ (π β NrmCVec β
((normCVβπ)β(0vecβπ)) β€ 1) |
16 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π§ = (0vecβπ) β
((normCVβπ)βπ§) = ((normCVβπ)β(0vecβπ))) |
17 | 16 | breq1d 5159 |
. . . . . . . . . . 11
β’ (π§ = (0vecβπ) β
(((normCVβπ)βπ§) β€ 1 β
((normCVβπ)β(0vecβπ)) β€ 1)) |
18 | 17 | rspcev 3613 |
. . . . . . . . . 10
β’
(((0vecβπ) β (BaseSetβπ) β§ ((normCVβπ)β(0vecβπ)) β€ 1) β βπ§ β (BaseSetβπ)((normCVβπ)βπ§) β€ 1) |
19 | 12, 15, 18 | syl2anc 585 |
. . . . . . . . 9
β’ (π β NrmCVec β
βπ§ β
(BaseSetβπ)((normCVβπ)βπ§) β€ 1) |
20 | 19 | biantrurd 534 |
. . . . . . . 8
β’ (π β NrmCVec β (π₯ = 0 β (βπ§ β (BaseSetβπ)((normCVβπ)βπ§) β€ 1 β§ π₯ = 0))) |
21 | 20 | adantr 482 |
. . . . . . 7
β’ ((π β NrmCVec β§ π β NrmCVec) β (π₯ = 0 β (βπ§ β (BaseSetβπ)((normCVβπ)βπ§) β€ 1 β§ π₯ = 0))) |
22 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(0vecβπ) = (0vecβπ) |
23 | 1, 22, 3 | 0oval 30041 |
. . . . . . . . . . . . . 14
β’ ((π β NrmCVec β§ π β NrmCVec β§ π§ β (BaseSetβπ)) β (πβπ§) = (0vecβπ)) |
24 | 23 | 3expa 1119 |
. . . . . . . . . . . . 13
β’ (((π β NrmCVec β§ π β NrmCVec) β§ π§ β (BaseSetβπ)) β (πβπ§) = (0vecβπ)) |
25 | 24 | fveq2d 6896 |
. . . . . . . . . . . 12
β’ (((π β NrmCVec β§ π β NrmCVec) β§ π§ β (BaseSetβπ)) β
((normCVβπ)β(πβπ§)) = ((normCVβπ)β(0vecβπ))) |
26 | 22, 6 | nvz0 29921 |
. . . . . . . . . . . . 13
β’ (π β NrmCVec β
((normCVβπ)β(0vecβπ)) = 0) |
27 | 26 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β NrmCVec β§ π β NrmCVec) β§ π§ β (BaseSetβπ)) β
((normCVβπ)β(0vecβπ)) = 0) |
28 | 25, 27 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (((π β NrmCVec β§ π β NrmCVec) β§ π§ β (BaseSetβπ)) β
((normCVβπ)β(πβπ§)) = 0) |
29 | 28 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (((π β NrmCVec β§ π β NrmCVec) β§ π§ β (BaseSetβπ)) β (π₯ = ((normCVβπ)β(πβπ§)) β π₯ = 0)) |
30 | 29 | anbi2d 630 |
. . . . . . . . 9
β’ (((π β NrmCVec β§ π β NrmCVec) β§ π§ β (BaseSetβπ)) β
((((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§))) β (((normCVβπ)βπ§) β€ 1 β§ π₯ = 0))) |
31 | 30 | rexbidva 3177 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π β NrmCVec) β
(βπ§ β
(BaseSetβπ)(((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§))) β βπ§ β (BaseSetβπ)(((normCVβπ)βπ§) β€ 1 β§ π₯ = 0))) |
32 | | r19.41v 3189 |
. . . . . . . 8
β’
(βπ§ β
(BaseSetβπ)(((normCVβπ)βπ§) β€ 1 β§ π₯ = 0) β (βπ§ β (BaseSetβπ)((normCVβπ)βπ§) β€ 1 β§ π₯ = 0)) |
33 | 31, 32 | bitr2di 288 |
. . . . . . 7
β’ ((π β NrmCVec β§ π β NrmCVec) β
((βπ§ β
(BaseSetβπ)((normCVβπ)βπ§) β€ 1 β§ π₯ = 0) β βπ§ β (BaseSetβπ)(((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§))))) |
34 | 21, 33 | bitrd 279 |
. . . . . 6
β’ ((π β NrmCVec β§ π β NrmCVec) β (π₯ = 0 β βπ§ β (BaseSetβπ)(((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§))))) |
35 | 34 | abbidv 2802 |
. . . . 5
β’ ((π β NrmCVec β§ π β NrmCVec) β {π₯ β£ π₯ = 0} = {π₯ β£ βπ§ β (BaseSetβπ)(((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))}) |
36 | 10, 35 | eqtr2id 2786 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec) β {π₯ β£ βπ§ β (BaseSetβπ)(((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))} = {0}) |
37 | 36 | supeq1d 9441 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec) β
sup({π₯ β£ βπ§ β (BaseSetβπ)(((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))}, β*, < ) = sup({0},
β*, < )) |
38 | 9, 37 | eqtrd 2773 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec) β (πβπ) = sup({0}, β*, <
)) |
39 | | xrltso 13120 |
. . 3
β’ < Or
β* |
40 | | 0xr 11261 |
. . 3
β’ 0 β
β* |
41 | | supsn 9467 |
. . 3
β’ (( <
Or β* β§ 0 β β*) β sup({0},
β*, < ) = 0) |
42 | 39, 40, 41 | mp2an 691 |
. 2
β’ sup({0},
β*, < ) = 0 |
43 | 38, 42 | eqtrdi 2789 |
1
β’ ((π β NrmCVec β§ π β NrmCVec) β (πβπ) = 0) |