Definition df-cpmat2mat 20332

Description: Transformation of a constant polynomial matrix (over a ring) into a matrix over the corresponding ring. Since this function is the inverse function of matToPolyMat, see m2cpminv 20384, it is also called "inverse matrix transformation" in the following. (Contributed by AV, 14-Dec-2019.)

Assertion

Ref	Expression
df-cpmat2mat	⊢ cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))

Distinct variable group:   𝑚,𝑛,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-cpmat2mat

Step	Hyp	Ref	Expression
1		ccpmat2mat 20329	. 2 class cPolyMatToMat
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 7841	. . 3 class Fin
5		cvv 3173	. . 3 class V
6		vm	. . . 4 setvar 𝑚
7	2	cv 1474	. . . . 5 class 𝑛
8	3	cv 1474	. . . . 5 class 𝑟
9		ccpmat 20327	. . . . 5 class ConstPolyMat
10	7, 8, 9	co 6549	. . . 4 class (𝑛 ConstPolyMat 𝑟)
11		vx	. . . . 5 setvar 𝑥
12		vy	. . . . 5 setvar 𝑦
13		cc0 9815	. . . . . 6 class 0
14	11	cv 1474	. . . . . . . 8 class 𝑥
15	12	cv 1474	. . . . . . . 8 class 𝑦
16	6	cv 1474	. . . . . . . 8 class 𝑚
17	14, 15, 16	co 6549	. . . . . . 7 class (𝑥𝑚𝑦)
18		cco1 19369	. . . . . . 7 class coe1
19	17, 18	cfv 5804	. . . . . 6 class (coe1‘(𝑥𝑚𝑦))
20	13, 19	cfv 5804	. . . . 5 class ((coe1‘(𝑥𝑚𝑦))‘0)
21	11, 12, 7, 7, 20	cmpt2 6551	. . . 4 class (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))
22	6, 10, 21	cmpt 4643	. . 3 class (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))
23	2, 3, 4, 5, 22	cmpt2 6551	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
24	1, 23	wceq 1475	1 wff cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))

This definition is referenced by:  cpm2mfval  20373