Step | Hyp | Ref
| Expression |
1 | | cscaf 20339 |
. 2
class
Β·sf |
2 | | vg |
. . 3
setvar π |
3 | | cvv 3448 |
. . 3
class
V |
4 | | vx |
. . . 4
setvar π₯ |
5 | | vy |
. . . 4
setvar π¦ |
6 | 2 | cv 1541 |
. . . . . 6
class π |
7 | | csca 17143 |
. . . . . 6
class
Scalar |
8 | 6, 7 | cfv 6501 |
. . . . 5
class
(Scalarβπ) |
9 | | cbs 17090 |
. . . . 5
class
Base |
10 | 8, 9 | cfv 6501 |
. . . 4
class
(Baseβ(Scalarβπ)) |
11 | 6, 9 | cfv 6501 |
. . . 4
class
(Baseβπ) |
12 | 4 | cv 1541 |
. . . . 5
class π₯ |
13 | 5 | cv 1541 |
. . . . 5
class π¦ |
14 | | cvsca 17144 |
. . . . . 6
class
Β·π |
15 | 6, 14 | cfv 6501 |
. . . . 5
class (
Β·π βπ) |
16 | 12, 13, 15 | co 7362 |
. . . 4
class (π₯(
Β·π βπ)π¦) |
17 | 4, 5, 10, 11, 16 | cmpo 7364 |
. . 3
class (π₯ β
(Baseβ(Scalarβπ)), π¦ β (Baseβπ) β¦ (π₯( Β·π
βπ)π¦)) |
18 | 2, 3, 17 | cmpt 5193 |
. 2
class (π β V β¦ (π₯ β
(Baseβ(Scalarβπ)), π¦ β (Baseβπ) β¦ (π₯( Β·π
βπ)π¦))) |
19 | 1, 18 | wceq 1542 |
1
wff
Β·sf = (π β V β¦ (π₯ β (Baseβ(Scalarβπ)), π¦ β (Baseβπ) β¦ (π₯( Β·π
βπ)π¦))) |