Detailed syntax breakdown of Definition df-cpmat2mat
| Step | Hyp | Ref
| Expression |
| 1 | | ccpmat2mat 22711 |
. 2
class
cPolyMatToMat |
| 2 | | vn |
. . 3
setvar 𝑛 |
| 3 | | vr |
. . 3
setvar 𝑟 |
| 4 | | cfn 8985 |
. . 3
class
Fin |
| 5 | | cvv 3480 |
. . 3
class
V |
| 6 | | vm |
. . . 4
setvar 𝑚 |
| 7 | 2 | cv 1539 |
. . . . 5
class 𝑛 |
| 8 | 3 | cv 1539 |
. . . . 5
class 𝑟 |
| 9 | | ccpmat 22709 |
. . . . 5
class
ConstPolyMat |
| 10 | 7, 8, 9 | co 7431 |
. . . 4
class (𝑛 ConstPolyMat 𝑟) |
| 11 | | vx |
. . . . 5
setvar 𝑥 |
| 12 | | vy |
. . . . 5
setvar 𝑦 |
| 13 | | cc0 11155 |
. . . . . 6
class
0 |
| 14 | 11 | cv 1539 |
. . . . . . . 8
class 𝑥 |
| 15 | 12 | cv 1539 |
. . . . . . . 8
class 𝑦 |
| 16 | 6 | cv 1539 |
. . . . . . . 8
class 𝑚 |
| 17 | 14, 15, 16 | co 7431 |
. . . . . . 7
class (𝑥𝑚𝑦) |
| 18 | | cco1 22179 |
. . . . . . 7
class
coe1 |
| 19 | 17, 18 | cfv 6561 |
. . . . . 6
class
(coe1‘(𝑥𝑚𝑦)) |
| 20 | 13, 19 | cfv 6561 |
. . . . 5
class
((coe1‘(𝑥𝑚𝑦))‘0) |
| 21 | 11, 12, 7, 7, 20 | cmpo 7433 |
. . . 4
class (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)) |
| 22 | 6, 10, 21 | cmpt 5225 |
. . 3
class (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))) |
| 23 | 2, 3, 4, 5, 22 | cmpo 7433 |
. 2
class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))) |
| 24 | 1, 23 | wceq 1540 |
1
wff
cPolyMatToMat = (𝑛 ∈
Fin, 𝑟 ∈ V ↦
(𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))) |