Step | Hyp | Ref
| Expression |
1 | | 0xr 11207 |
. . 3
β’ 0 β
β* |
2 | 1 | a1i 11 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β 0 β
β*) |
3 | | simp2 1138 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β π β NrmCVec) |
4 | | nmoxr.1 |
. . . . . . . 8
β’ π = (BaseSetβπ) |
5 | | eqid 2733 |
. . . . . . . 8
β’
(0vecβπ) = (0vecβπ) |
6 | 4, 5 | nvzcl 29618 |
. . . . . . 7
β’ (π β NrmCVec β
(0vecβπ)
β π) |
7 | | ffvelcdm 7033 |
. . . . . . 7
β’ ((π:πβΆπ β§ (0vecβπ) β π) β (πβ(0vecβπ)) β π) |
8 | 6, 7 | sylan2 594 |
. . . . . 6
β’ ((π:πβΆπ β§ π β NrmCVec) β (πβ(0vecβπ)) β π) |
9 | 8 | ancoms 460 |
. . . . 5
β’ ((π β NrmCVec β§ π:πβΆπ) β (πβ(0vecβπ)) β π) |
10 | 9 | 3adant2 1132 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β (πβ(0vecβπ)) β π) |
11 | | nmoxr.2 |
. . . . 5
β’ π = (BaseSetβπ) |
12 | | eqid 2733 |
. . . . 5
β’
(normCVβπ) = (normCVβπ) |
13 | 11, 12 | nvcl 29645 |
. . . 4
β’ ((π β NrmCVec β§ (πβ(0vecβπ)) β π) β ((normCVβπ)β(πβ(0vecβπ))) β
β) |
14 | 3, 10, 13 | syl2anc 585 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β ((normCVβπ)β(πβ(0vecβπ))) β
β) |
15 | 14 | rexrd 11210 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β ((normCVβπ)β(πβ(0vecβπ))) β
β*) |
16 | | nmoxr.3 |
. . 3
β’ π = (π normOpOLD π) |
17 | 4, 11, 16 | nmoxr 29750 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β (πβπ) β
β*) |
18 | 11, 12 | nvge0 29657 |
. . 3
β’ ((π β NrmCVec β§ (πβ(0vecβπ)) β π) β 0 β€
((normCVβπ)β(πβ(0vecβπ)))) |
19 | 3, 10, 18 | syl2anc 585 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β 0 β€
((normCVβπ)β(πβ(0vecβπ)))) |
20 | 11, 12 | nmosetre 29748 |
. . . . . . 7
β’ ((π β NrmCVec β§ π:πβΆπ) β {π₯ β£ βπ§ β π (((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))} β β) |
21 | | ressxr 11204 |
. . . . . . 7
β’ β
β β* |
22 | 20, 21 | sstrdi 3957 |
. . . . . 6
β’ ((π β NrmCVec β§ π:πβΆπ) β {π₯ β£ βπ§ β π (((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))} β
β*) |
23 | | eqid 2733 |
. . . . . . 7
β’
(normCVβπ) = (normCVβπ) |
24 | 4, 5, 23 | nmosetn0 29749 |
. . . . . 6
β’ (π β NrmCVec β
((normCVβπ)β(πβ(0vecβπ))) β {π₯ β£ βπ§ β π (((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))}) |
25 | | supxrub 13249 |
. . . . . 6
β’ (({π₯ β£ βπ§ β π (((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))} β β* β§
((normCVβπ)β(πβ(0vecβπ))) β {π₯ β£ βπ§ β π (((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))}) β ((normCVβπ)β(πβ(0vecβπ))) β€ sup({π₯ β£ βπ§ β π (((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))}, β*, <
)) |
26 | 22, 24, 25 | syl2an 597 |
. . . . 5
β’ (((π β NrmCVec β§ π:πβΆπ) β§ π β NrmCVec) β
((normCVβπ)β(πβ(0vecβπ))) β€ sup({π₯ β£ βπ§ β π (((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))}, β*, <
)) |
27 | 26 | 3impa 1111 |
. . . 4
β’ ((π β NrmCVec β§ π:πβΆπ β§ π β NrmCVec) β
((normCVβπ)β(πβ(0vecβπ))) β€ sup({π₯ β£ βπ§ β π (((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))}, β*, <
)) |
28 | 27 | 3comr 1126 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β ((normCVβπ)β(πβ(0vecβπ))) β€ sup({π₯ β£ βπ§ β π (((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))}, β*, <
)) |
29 | 4, 11, 23, 12, 16 | nmooval 29747 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β (πβπ) = sup({π₯ β£ βπ§ β π (((normCVβπ)βπ§) β€ 1 β§ π₯ = ((normCVβπ)β(πβπ§)))}, β*, <
)) |
30 | 28, 29 | breqtrrd 5134 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β ((normCVβπ)β(πβ(0vecβπ))) β€ (πβπ)) |
31 | 2, 15, 17, 19, 30 | xrletrd 13087 |
1
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β 0 β€ (πβπ)) |