Detailed syntax breakdown of Definition df-mat2pmat
Step | Hyp | Ref
| Expression |
1 | | cmat2pmat 21458 |
. 2
class
matToPolyMat |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cfn 8558 |
. . 3
class
Fin |
5 | | cvv 3399 |
. . 3
class
V |
6 | | vm |
. . . 4
setvar 𝑚 |
7 | 2 | cv 1541 |
. . . . . 6
class 𝑛 |
8 | 3 | cv 1541 |
. . . . . 6
class 𝑟 |
9 | | cmat 21161 |
. . . . . 6
class
Mat |
10 | 7, 8, 9 | co 7173 |
. . . . 5
class (𝑛 Mat 𝑟) |
11 | | cbs 16589 |
. . . . 5
class
Base |
12 | 10, 11 | cfv 6340 |
. . . 4
class
(Base‘(𝑛 Mat
𝑟)) |
13 | | vx |
. . . . 5
setvar 𝑥 |
14 | | vy |
. . . . 5
setvar 𝑦 |
15 | 13 | cv 1541 |
. . . . . . 7
class 𝑥 |
16 | 14 | cv 1541 |
. . . . . . 7
class 𝑦 |
17 | 6 | cv 1541 |
. . . . . . 7
class 𝑚 |
18 | 15, 16, 17 | co 7173 |
. . . . . 6
class (𝑥𝑚𝑦) |
19 | | cpl1 20955 |
. . . . . . . 8
class
Poly1 |
20 | 8, 19 | cfv 6340 |
. . . . . . 7
class
(Poly1‘𝑟) |
21 | | cascl 20671 |
. . . . . . 7
class
algSc |
22 | 20, 21 | cfv 6340 |
. . . . . 6
class
(algSc‘(Poly1‘𝑟)) |
23 | 18, 22 | cfv 6340 |
. . . . 5
class
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)) |
24 | 13, 14, 7, 7, 23 | cmpo 7175 |
. . . 4
class (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦))) |
25 | 6, 12, 24 | cmpt 5111 |
. . 3
class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))) |
26 | 2, 3, 4, 5, 25 | cmpo 7175 |
. 2
class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦))))) |
27 | 1, 26 | wceq 1542 |
1
wff
matToPolyMat = (𝑛 ∈
Fin, 𝑟 ∈ V ↦
(𝑚 ∈
(Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦))))) |