Step | Hyp | Ref
| Expression |
1 | | nmoofval.6 |
. 2
β’ π = (π normOpOLD π) |
2 | | fveq2 6843 |
. . . . . 6
β’ (π’ = π β (BaseSetβπ’) = (BaseSetβπ)) |
3 | | nmoofval.1 |
. . . . . 6
β’ π = (BaseSetβπ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . 5
β’ (π’ = π β (BaseSetβπ’) = π) |
5 | 4 | oveq2d 7374 |
. . . 4
β’ (π’ = π β ((BaseSetβπ€) βm (BaseSetβπ’)) = ((BaseSetβπ€) βm π)) |
6 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π’ = π β (normCVβπ’) =
(normCVβπ)) |
7 | | nmoofval.3 |
. . . . . . . . . . 11
β’ πΏ =
(normCVβπ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π’ = π β (normCVβπ’) = πΏ) |
9 | 8 | fveq1d 6845 |
. . . . . . . . 9
β’ (π’ = π β ((normCVβπ’)βπ§) = (πΏβπ§)) |
10 | 9 | breq1d 5116 |
. . . . . . . 8
β’ (π’ = π β (((normCVβπ’)βπ§) β€ 1 β (πΏβπ§) β€ 1)) |
11 | 10 | anbi1d 631 |
. . . . . . 7
β’ (π’ = π β ((((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§))) β ((πΏβπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§))))) |
12 | 4, 11 | rexeqbidv 3319 |
. . . . . 6
β’ (π’ = π β (βπ§ β (BaseSetβπ’)(((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§))) β βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§))))) |
13 | 12 | abbidv 2802 |
. . . . 5
β’ (π’ = π β {π₯ β£ βπ§ β (BaseSetβπ’)(((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))} = {π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))}) |
14 | 13 | supeq1d 9387 |
. . . 4
β’ (π’ = π β sup({π₯ β£ βπ§ β (BaseSetβπ’)(((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))}, β*, < ) =
sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))}, β*, <
)) |
15 | 5, 14 | mpteq12dv 5197 |
. . 3
β’ (π’ = π β (π‘ β ((BaseSetβπ€) βm (BaseSetβπ’)) β¦ sup({π₯ β£ βπ§ β (BaseSetβπ’)(((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))}, β*, < )) = (π‘ β ((BaseSetβπ€) βm π) β¦ sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))}, β*, <
))) |
16 | | fveq2 6843 |
. . . . . 6
β’ (π€ = π β (BaseSetβπ€) = (BaseSetβπ)) |
17 | | nmoofval.2 |
. . . . . 6
β’ π = (BaseSetβπ) |
18 | 16, 17 | eqtr4di 2791 |
. . . . 5
β’ (π€ = π β (BaseSetβπ€) = π) |
19 | 18 | oveq1d 7373 |
. . . 4
β’ (π€ = π β ((BaseSetβπ€) βm π) = (π βm π)) |
20 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π€ = π β (normCVβπ€) =
(normCVβπ)) |
21 | | nmoofval.4 |
. . . . . . . . . . 11
β’ π =
(normCVβπ) |
22 | 20, 21 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π€ = π β (normCVβπ€) = π) |
23 | 22 | fveq1d 6845 |
. . . . . . . . 9
β’ (π€ = π β ((normCVβπ€)β(π‘βπ§)) = (πβ(π‘βπ§))) |
24 | 23 | eqeq2d 2744 |
. . . . . . . 8
β’ (π€ = π β (π₯ = ((normCVβπ€)β(π‘βπ§)) β π₯ = (πβ(π‘βπ§)))) |
25 | 24 | anbi2d 630 |
. . . . . . 7
β’ (π€ = π β (((πΏβπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§))) β ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§))))) |
26 | 25 | rexbidv 3172 |
. . . . . 6
β’ (π€ = π β (βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§))) β βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§))))) |
27 | 26 | abbidv 2802 |
. . . . 5
β’ (π€ = π β {π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))} = {π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))}) |
28 | 27 | supeq1d 9387 |
. . . 4
β’ (π€ = π β sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))}, β*, < ) =
sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))}, β*, <
)) |
29 | 19, 28 | mpteq12dv 5197 |
. . 3
β’ (π€ = π β (π‘ β ((BaseSetβπ€) βm π) β¦ sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))}, β*, < )) = (π‘ β (π βm π) β¦ sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))}, β*, <
))) |
30 | | df-nmoo 29729 |
. . 3
β’
normOpOLD = (π’
β NrmCVec, π€ β
NrmCVec β¦ (π‘ β
((BaseSetβπ€)
βm (BaseSetβπ’)) β¦ sup({π₯ β£ βπ§ β (BaseSetβπ’)(((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))}, β*, <
))) |
31 | | ovex 7391 |
. . . 4
β’ (π βm π) β V |
32 | 31 | mptex 7174 |
. . 3
β’ (π‘ β (π βm π) β¦ sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))}, β*, < )) β
V |
33 | 15, 29, 30, 32 | ovmpo 7516 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec) β (π normOpOLD π) = (π‘ β (π βm π) β¦ sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))}, β*, <
))) |
34 | 1, 33 | eqtrid 2785 |
1
β’ ((π β NrmCVec β§ π β NrmCVec) β π = (π‘ β (π βm π) β¦ sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))}, β*, <
))) |