Step | Hyp | Ref
| Expression |
1 | | cmat2pmat 22427 |
. 2
class
matToPolyMat |
2 | | vn |
. . 3
setvar π |
3 | | vr |
. . 3
setvar π |
4 | | cfn 8943 |
. . 3
class
Fin |
5 | | cvv 3473 |
. . 3
class
V |
6 | | vm |
. . . 4
setvar π |
7 | 2 | cv 1539 |
. . . . . 6
class π |
8 | 3 | cv 1539 |
. . . . . 6
class π |
9 | | cmat 22128 |
. . . . . 6
class
Mat |
10 | 7, 8, 9 | co 7412 |
. . . . 5
class (π Mat π) |
11 | | cbs 17149 |
. . . . 5
class
Base |
12 | 10, 11 | cfv 6543 |
. . . 4
class
(Baseβ(π Mat
π)) |
13 | | vx |
. . . . 5
setvar π₯ |
14 | | vy |
. . . . 5
setvar π¦ |
15 | 13 | cv 1539 |
. . . . . . 7
class π₯ |
16 | 14 | cv 1539 |
. . . . . . 7
class π¦ |
17 | 6 | cv 1539 |
. . . . . . 7
class π |
18 | 15, 16, 17 | co 7412 |
. . . . . 6
class (π₯ππ¦) |
19 | | cpl1 21921 |
. . . . . . . 8
class
Poly1 |
20 | 8, 19 | cfv 6543 |
. . . . . . 7
class
(Poly1βπ) |
21 | | cascl 21627 |
. . . . . . 7
class
algSc |
22 | 20, 21 | cfv 6543 |
. . . . . 6
class
(algScβ(Poly1βπ)) |
23 | 18, 22 | cfv 6543 |
. . . . 5
class
((algScβ(Poly1βπ))β(π₯ππ¦)) |
24 | 13, 14, 7, 7, 23 | cmpo 7414 |
. . . 4
class (π₯ β π, π¦ β π β¦
((algScβ(Poly1βπ))β(π₯ππ¦))) |
25 | 6, 12, 24 | cmpt 5231 |
. . 3
class (π β (Baseβ(π Mat π)) β¦ (π₯ β π, π¦ β π β¦
((algScβ(Poly1βπ))β(π₯ππ¦)))) |
26 | 2, 3, 4, 5, 25 | cmpo 7414 |
. 2
class (π β Fin, π β V β¦ (π β (Baseβ(π Mat π)) β¦ (π₯ β π, π¦ β π β¦
((algScβ(Poly1βπ))β(π₯ππ¦))))) |
27 | 1, 26 | wceq 1540 |
1
wff
matToPolyMat = (π β
Fin, π β V β¦
(π β
(Baseβ(π Mat π)) β¦ (π₯ β π, π¦ β π β¦
((algScβ(Poly1βπ))β(π₯ππ¦))))) |