Definition df-decpmat 20568

Description: Define the decomposition of polynomial matrices. This function collects the coefficients of a polynomial matrix m belong to the k th power of the polynomial variable for each entry of m. (Contributed by AV, 2-Dec-2019.)

Assertion

Ref	Expression
df-decpmat	|- decompPMat = ( m e. _V , k e. NN0 |-> ( i e. dom dom m , j e. dom dom m |-> ( (coe1 ` ( i m j ) ) ` k ) ) )

Distinct variable group:   i, j, k, m

Detailed syntax breakdown of Definition df-decpmat

Step	Hyp	Ref	Expression
1		cdecpmat 20567	. 2 class decompPMat
2		vm	. . 3 setvar m
3		vk	. . 3 setvar k
4		cvv 3200	. . 3 class _V
5		cn0 11292	. . 3 class NN0
6		vi	. . . 4 setvar i
7		vj	. . . 4 setvar j
8	2	cv 1482	. . . . . 6 class m
9	8	cdm 5114	. . . . 5 class dom m
10	9	cdm 5114	. . . 4 class dom dom m
11	3	cv 1482	. . . . 5 class k
12	6	cv 1482	. . . . . . 7 class i
13	7	cv 1482	. . . . . . 7 class j
14	12, 13, 8	co 6650	. . . . . 6 class ( i m j )
15		cco1 19548	. . . . . 6 class coe1
16	14, 15	cfv 5888	. . . . 5 class (coe1 ` ( i m j ) )
17	11, 16	cfv 5888	. . . 4 class ( (coe1 ` ( i m j ) ) ` k )
18	6, 7, 10, 10, 17	cmpt2 6652	. . 3 class ( i e. dom dom m , j e. dom dom m |-> ( (coe1 ` ( i m j ) ) ` k ) )
19	2, 3, 4, 5, 18	cmpt2 6652	. 2 class ( m e. _V , k e. NN0 |-> ( i e. dom dom m , j e. dom dom m |-> ( (coe1 ` ( i m j ) ) ` k ) ) )
20	1, 19	wceq 1483	1 wff decompPMat = ( m e. _V , k e. NN0 |-> ( i e. dom dom m , j e. dom dom m |-> ( (coe1 ` ( i m j ) ) ` k ) ) )

This definition is referenced by:  decpmatval0  20569  pmatcollpw3lem  20588