Step | Hyp | Ref
| Expression |
1 | | cnmoo 30025 |
. 2
class
normOpOLD |
2 | | vu |
. . 3
setvar π’ |
3 | | vw |
. . 3
setvar π€ |
4 | | cnv 29868 |
. . 3
class
NrmCVec |
5 | | vt |
. . . 4
setvar π‘ |
6 | 3 | cv 1541 |
. . . . . 6
class π€ |
7 | | cba 29870 |
. . . . . 6
class
BaseSet |
8 | 6, 7 | cfv 6544 |
. . . . 5
class
(BaseSetβπ€) |
9 | 2 | cv 1541 |
. . . . . 6
class π’ |
10 | 9, 7 | cfv 6544 |
. . . . 5
class
(BaseSetβπ’) |
11 | | cmap 8820 |
. . . . 5
class
βm |
12 | 8, 10, 11 | co 7409 |
. . . 4
class
((BaseSetβπ€)
βm (BaseSetβπ’)) |
13 | | vz |
. . . . . . . . . . 11
setvar π§ |
14 | 13 | cv 1541 |
. . . . . . . . . 10
class π§ |
15 | | cnmcv 29874 |
. . . . . . . . . . 11
class
normCV |
16 | 9, 15 | cfv 6544 |
. . . . . . . . . 10
class
(normCVβπ’) |
17 | 14, 16 | cfv 6544 |
. . . . . . . . 9
class
((normCVβπ’)βπ§) |
18 | | c1 11111 |
. . . . . . . . 9
class
1 |
19 | | cle 11249 |
. . . . . . . . 9
class
β€ |
20 | 17, 18, 19 | wbr 5149 |
. . . . . . . 8
wff
((normCVβπ’)βπ§) β€ 1 |
21 | | vx |
. . . . . . . . . 10
setvar π₯ |
22 | 21 | cv 1541 |
. . . . . . . . 9
class π₯ |
23 | 5 | cv 1541 |
. . . . . . . . . . 11
class π‘ |
24 | 14, 23 | cfv 6544 |
. . . . . . . . . 10
class (π‘βπ§) |
25 | 6, 15 | cfv 6544 |
. . . . . . . . . 10
class
(normCVβπ€) |
26 | 24, 25 | cfv 6544 |
. . . . . . . . 9
class
((normCVβπ€)β(π‘βπ§)) |
27 | 22, 26 | wceq 1542 |
. . . . . . . 8
wff π₯ =
((normCVβπ€)β(π‘βπ§)) |
28 | 20, 27 | wa 397 |
. . . . . . 7
wff
(((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§))) |
29 | 28, 13, 10 | wrex 3071 |
. . . . . 6
wff
βπ§ β
(BaseSetβπ’)(((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§))) |
30 | 29, 21 | cab 2710 |
. . . . 5
class {π₯ β£ βπ§ β (BaseSetβπ’)(((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))} |
31 | | cxr 11247 |
. . . . 5
class
β* |
32 | | clt 11248 |
. . . . 5
class
< |
33 | 30, 31, 32 | csup 9435 |
. . . 4
class
sup({π₯ β£
βπ§ β
(BaseSetβπ’)(((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))}, β*, <
) |
34 | 5, 12, 33 | cmpt 5232 |
. . 3
class (π‘ β ((BaseSetβπ€) βm
(BaseSetβπ’)) β¦
sup({π₯ β£ βπ§ β (BaseSetβπ’)(((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))}, β*, <
)) |
35 | 2, 3, 4, 4, 34 | cmpo 7411 |
. 2
class (π’ β NrmCVec, π€ β NrmCVec β¦ (π‘ β ((BaseSetβπ€) βm
(BaseSetβπ’)) β¦
sup({π₯ β£ βπ§ β (BaseSetβπ’)(((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))}, β*, <
))) |
36 | 1, 35 | wceq 1542 |
1
wff
normOpOLD = (π’
β NrmCVec, π€ β
NrmCVec β¦ (π‘ β
((BaseSetβπ€)
βm (BaseSetβπ’)) β¦ sup({π₯ β£ βπ§ β (BaseSetβπ’)(((normCVβπ’)βπ§) β€ 1 β§ π₯ = ((normCVβπ€)β(π‘βπ§)))}, β*, <
))) |