Step | Hyp | Ref
| Expression |
1 | | cocv 21087 |
. 2
class
ocv |
2 | | vh |
. . 3
setvar β |
3 | | cvv 3447 |
. . 3
class
V |
4 | | vs |
. . . 4
setvar π |
5 | 2 | cv 1541 |
. . . . . 6
class β |
6 | | cbs 17091 |
. . . . . 6
class
Base |
7 | 5, 6 | cfv 6500 |
. . . . 5
class
(Baseββ) |
8 | 7 | cpw 4564 |
. . . 4
class π«
(Baseββ) |
9 | | vx |
. . . . . . . . 9
setvar π₯ |
10 | 9 | cv 1541 |
. . . . . . . 8
class π₯ |
11 | | vy |
. . . . . . . . 9
setvar π¦ |
12 | 11 | cv 1541 |
. . . . . . . 8
class π¦ |
13 | | cip 17146 |
. . . . . . . . 9
class
Β·π |
14 | 5, 13 | cfv 6500 |
. . . . . . . 8
class
(Β·πββ) |
15 | 10, 12, 14 | co 7361 |
. . . . . . 7
class (π₯(Β·πββ)π¦) |
16 | | csca 17144 |
. . . . . . . . 9
class
Scalar |
17 | 5, 16 | cfv 6500 |
. . . . . . . 8
class
(Scalarββ) |
18 | | c0g 17329 |
. . . . . . . 8
class
0g |
19 | 17, 18 | cfv 6500 |
. . . . . . 7
class
(0gβ(Scalarββ)) |
20 | 15, 19 | wceq 1542 |
. . . . . 6
wff (π₯(Β·πββ)π¦) = (0gβ(Scalarββ)) |
21 | 4 | cv 1541 |
. . . . . 6
class π |
22 | 20, 11, 21 | wral 3061 |
. . . . 5
wff
βπ¦ β
π (π₯(Β·πββ)π¦) = (0gβ(Scalarββ)) |
23 | 22, 9, 7 | crab 3406 |
. . . 4
class {π₯ β (Baseββ) β£ βπ¦ β π (π₯(Β·πββ)π¦) = (0gβ(Scalarββ))} |
24 | 4, 8, 23 | cmpt 5192 |
. . 3
class (π β π«
(Baseββ) β¦
{π₯ β (Baseββ) β£ βπ¦ β π (π₯(Β·πββ)π¦) = (0gβ(Scalarββ))}) |
25 | 2, 3, 24 | cmpt 5192 |
. 2
class (β β V β¦ (π β π«
(Baseββ) β¦
{π₯ β (Baseββ) β£ βπ¦ β π (π₯(Β·πββ)π¦) = (0gβ(Scalarββ))})) |
26 | 1, 25 | wceq 1542 |
1
wff ocv =
(β β V β¦ (π β π«
(Baseββ) β¦
{π₯ β (Baseββ) β£ βπ¦ β π (π₯(Β·πββ)π¦) = (0gβ(Scalarββ))})) |