Definition df-decpmat

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdecpmat	|- decompPMat
1		vm	|- m
2		cvv	|- _V
3		vk	|- k
4		cn0	|- NN0
5		vi	|- i
6	1	cv	|- m
7	6	cdm	|- dom m
8	7	cdm	|- dom dom m
9		vj	|- j
10		cco1	|- coe1
11	5	cv	|- i
12	9	cv	|- j
13	11 12 6	co	|- ( i m j )
14	13 10	cfv	|- ( coe1 ` ( i m j ) )
15	3	cv	|- k
16	15 14	cfv	|- ( ( coe1 ` ( i m j ) ) ` k )
17	5 9 8 8 16	cmpo	|- ( i e. dom dom m , j e. dom dom m |-> ( ( coe1 ` ( i m j ) ) ` k ) )
18	1 3 2 4 17	cmpo	|- ( m e. _V , k e. NN0 |-> ( i e. dom dom m , j e. dom dom m |-> ( ( coe1 ` ( i m j ) ) ` k ) ) )
19	0 18	wceq	|- decompPMat = ( m e. _V , k e. NN0 |-> ( i e. dom dom m , j e. dom dom m |-> ( ( coe1 ` ( i m j ) ) ` k ) ) )