Step | Hyp | Ref
| Expression |
1 | | nmoofval.2 |
. . . . 5
β’ π = (BaseSetβπ) |
2 | 1 | fvexi 6857 |
. . . 4
β’ π β V |
3 | | nmoofval.1 |
. . . . 5
β’ π = (BaseSetβπ) |
4 | 3 | fvexi 6857 |
. . . 4
β’ π β V |
5 | 2, 4 | elmap 8812 |
. . 3
β’ (π β (π βm π) β π:πβΆπ) |
6 | | nmoofval.3 |
. . . . . 6
β’ πΏ =
(normCVβπ) |
7 | | nmoofval.4 |
. . . . . 6
β’ π =
(normCVβπ) |
8 | | nmoofval.6 |
. . . . . 6
β’ π = (π normOpOLD π) |
9 | 3, 1, 6, 7, 8 | nmoofval 29746 |
. . . . 5
β’ ((π β NrmCVec β§ π β NrmCVec) β π = (π‘ β (π βm π) β¦ sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))}, β*, <
))) |
10 | 9 | fveq1d 6845 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec) β (πβπ) = ((π‘ β (π βm π) β¦ sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))}, β*, <
))βπ)) |
11 | | fveq1 6842 |
. . . . . . . . . . 11
β’ (π‘ = π β (π‘βπ§) = (πβπ§)) |
12 | 11 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π‘ = π β (πβ(π‘βπ§)) = (πβ(πβπ§))) |
13 | 12 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π‘ = π β (π₯ = (πβ(π‘βπ§)) β π₯ = (πβ(πβπ§)))) |
14 | 13 | anbi2d 630 |
. . . . . . . 8
β’ (π‘ = π β (((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§))) β ((πΏβπ§) β€ 1 β§ π₯ = (πβ(πβπ§))))) |
15 | 14 | rexbidv 3172 |
. . . . . . 7
β’ (π‘ = π β (βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§))) β βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(πβπ§))))) |
16 | 15 | abbidv 2802 |
. . . . . 6
β’ (π‘ = π β {π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))} = {π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(πβπ§)))}) |
17 | 16 | supeq1d 9387 |
. . . . 5
β’ (π‘ = π β sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))}, β*, < ) =
sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(πβπ§)))}, β*, <
)) |
18 | | eqid 2733 |
. . . . 5
β’ (π‘ β (π βm π) β¦ sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))}, β*, < )) = (π‘ β (π βm π) β¦ sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))}, β*, <
)) |
19 | | xrltso 13066 |
. . . . . 6
β’ < Or
β* |
20 | 19 | supex 9404 |
. . . . 5
β’
sup({π₯ β£
βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(πβπ§)))}, β*, < ) β
V |
21 | 17, 18, 20 | fvmpt 6949 |
. . . 4
β’ (π β (π βm π) β ((π‘ β (π βm π) β¦ sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(π‘βπ§)))}, β*, <
))βπ) = sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(πβπ§)))}, β*, <
)) |
22 | 10, 21 | sylan9eq 2793 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec) β§ π β (π βm π)) β (πβπ) = sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(πβπ§)))}, β*, <
)) |
23 | 5, 22 | sylan2br 596 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec) β§ π:πβΆπ) β (πβπ) = sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(πβπ§)))}, β*, <
)) |
24 | 23 | 3impa 1111 |
1
β’ ((π β NrmCVec β§ π β NrmCVec β§ π:πβΆπ) β (πβπ) = sup({π₯ β£ βπ§ β π ((πΏβπ§) β€ 1 β§ π₯ = (πβ(πβπ§)))}, β*, <
)) |