Definition df-cpmat2mat 20513

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 20565, it is also called "inverse matrix transformation" in the following. (Contributed by AV, 14-Dec-2019.)

Assertion

Ref	Expression
df-cpmat2mat	|- cPolyMatToMat = ( n e. Fin , r e. _V |-> ( m e. ( n ConstPolyMat r ) |-> ( x e. n , y e. n |-> ( (coe1 ` ( x m y ) ) ` 0 ) ) ) )

Distinct variable group:   m, n, r, x, y

Detailed syntax breakdown of Definition df-cpmat2mat

Step	Hyp	Ref	Expression
1		ccpmat2mat 20510	. 2 class cPolyMatToMat
2		vn	. . 3 setvar n
3		vr	. . 3 setvar r
4		cfn 7955	. . 3 class Fin
5		cvv 3200	. . 3 class _V
6		vm	. . . 4 setvar m
7	2	cv 1482	. . . . 5 class n
8	3	cv 1482	. . . . 5 class r
9		ccpmat 20508	. . . . 5 class ConstPolyMat
10	7, 8, 9	co 6650	. . . 4 class ( n ConstPolyMat r )
11		vx	. . . . 5 setvar x
12		vy	. . . . 5 setvar y
13		cc0 9936	. . . . . 6 class 0
14	11	cv 1482	. . . . . . . 8 class x
15	12	cv 1482	. . . . . . . 8 class y
16	6	cv 1482	. . . . . . . 8 class m
17	14, 15, 16	co 6650	. . . . . . 7 class ( x m y )
18		cco1 19548	. . . . . . 7 class coe1
19	17, 18	cfv 5888	. . . . . 6 class (coe1 ` ( x m y ) )
20	13, 19	cfv 5888	. . . . 5 class ( (coe1 ` ( x m y ) ) ` 0 )
21	11, 12, 7, 7, 20	cmpt2 6652	. . . 4 class ( x e. n , y e. n |-> ( (coe1 ` ( x m y ) ) ` 0 ) )
22	6, 10, 21	cmpt 4729	. . 3 class ( m e. ( n ConstPolyMat r ) |-> ( x e. n , y e. n |-> ( (coe1 ` ( x m y ) ) ` 0 ) ) )
23	2, 3, 4, 5, 22	cmpt2 6652	. 2 class ( n e. Fin , r e. _V |-> ( m e. ( n ConstPolyMat r ) |-> ( x e. n , y e. n |-> ( (coe1 ` ( x m y ) ) ` 0 ) ) ) )
24	1, 23	wceq 1483	1 wff cPolyMatToMat = ( n e. Fin , r e. _V |-> ( m e. ( n ConstPolyMat r ) |-> ( x e. n , y e. n |-> ( (coe1 ` ( x m y ) ) ` 0 ) ) ) )

This definition is referenced by:  cpm2mfval  20554