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	$$⊢\mathrm{decompPMat}=\left(m\in \mathrm{V},k\in {\mathbb{N}}_0⟼\left(i\in \mathrm{dom}\mathrm{dom}m,j\in \mathrm{dom}\mathrm{dom}m⟼{\mathrm{coe}}_1\left(imj\right)\left(k\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdecpmat	$$class\mathrm{decompPMat}$$
1		vm	$$setvarm$$
2		cvv	$$class\mathrm{V}$$
3		vk	$$setvark$$
4		cn0	$$class{\mathbb{N}}_0$$
5		vi	$$setvari$$
6	1	cv	$$setvarm$$
7	6	cdm	$$class\mathrm{dom}m$$
8	7	cdm	$$class\mathrm{dom}\mathrm{dom}m$$
9		vj	$$setvarj$$
10		cco1	$$class{\mathrm{coe}}_1$$
11	5	cv	$$setvari$$
12	9	cv	$$setvarj$$
13	11 12 6	co	$$class\left(imj\right)$$
14	13 10	cfv	$$class{\mathrm{coe}}_1\left(imj\right)$$
15	3	cv	$$setvark$$
16	15 14	cfv	$$class{\mathrm{coe}}_1\left(imj\right)\left(k\right)$$
17	5 9 8 8 16	cmpo	$$class\left(i\in \mathrm{dom}\mathrm{dom}m,j\in \mathrm{dom}\mathrm{dom}m⟼{\mathrm{coe}}_1\left(imj\right)\left(k\right)\right)$$
18	1 3 2 4 17	cmpo	$$class\left(m\in \mathrm{V},k\in {\mathbb{N}}_0⟼\left(i\in \mathrm{dom}\mathrm{dom}m,j\in \mathrm{dom}\mathrm{dom}m⟼{\mathrm{coe}}_1\left(imj\right)\left(k\right)\right)\right)$$
19	0 18	wceq	$$wff\mathrm{decompPMat}=\left(m\in \mathrm{V},k\in {\mathbb{N}}_0⟼\left(i\in \mathrm{dom}\mathrm{dom}m,j\in \mathrm{dom}\mathrm{dom}m⟼{\mathrm{coe}}_1\left(imj\right)\left(k\right)\right)\right)$$