Definition df-cpmat2mat 22915

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 22967, 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 22912	. 2 class cPolyMatToMat
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8949	. . 3 class Fin
5		cvv 3457	. . 3 class V
6		vm	. . . 4 setvar 𝑚
7	2	cv 1569	. . . . 5 class 𝑛
8	3	cv 1569	. . . . 5 class 𝑟
9		ccpmat 22910	. . . . 5 class ConstPolyMat
10	7, 8, 9	co 7419	. . . 4 class (𝑛 ConstPolyMat 𝑟)
11		vx	. . . . 5 setvar 𝑥
12		vy	. . . . 5 setvar 𝑦
13		cc0 11115	. . . . . 6 class 0
14	11	cv 1569	. . . . . . . 8 class 𝑥
15	12	cv 1569	. . . . . . . 8 class 𝑦
16	6	cv 1569	. . . . . . . 8 class 𝑚
17	14, 15, 16	co 7419	. . . . . . 7 class (𝑥𝑚𝑦)
18		cco1 22388	. . . . . . 7 class coe1
19	17, 18	cfv 6540	. . . . . 6 class (coe1‘(𝑥𝑚𝑦))
20	13, 19	cfv 6540	. . . . 5 class ((coe1‘(𝑥𝑚𝑦))‘0)
21	11, 12, 7, 7, 20	cmpo 7421	. . . 4 class (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))
22	6, 10, 21	cmpt 5194	. . 3 class (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))
23	2, 3, 4, 5, 22	cmpo 7421	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
24	1, 23	wceq 1570	1 wff cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))

This definition is used by:  cpm2mfval  22956