Definition df-decpmat 21660

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

Assertion

Ref	Expression
df-decpmat	⊢ decompPMat = (𝑚 ∈ V, 𝑘 ∈ ℕ0 ↦ (𝑖 ∈ dom dom 𝑚, 𝑗 ∈ dom dom 𝑚 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)))

Distinct variable group:   𝑖,𝑗,𝑘,𝑚

Detailed syntax breakdown of Definition df-decpmat

Step	Hyp	Ref	Expression
1		cdecpmat 21659	. 2 class decompPMat
2		vm	. . 3 setvar 𝑚
3		vk	. . 3 setvar 𝑘
4		cvv 3408	. . 3 class V
5		cn0 12090	. . 3 class ℕ0
6		vi	. . . 4 setvar 𝑖
7		vj	. . . 4 setvar 𝑗
8	2	cv 1542	. . . . . 6 class 𝑚
9	8	cdm 5551	. . . . 5 class dom 𝑚
10	9	cdm 5551	. . . 4 class dom dom 𝑚
11	3	cv 1542	. . . . 5 class 𝑘
12	6	cv 1542	. . . . . . 7 class 𝑖
13	7	cv 1542	. . . . . . 7 class 𝑗
14	12, 13, 8	co 7213	. . . . . 6 class (𝑖𝑚𝑗)
15		cco1 21099	. . . . . 6 class coe1
16	14, 15	cfv 6380	. . . . 5 class (coe1‘(𝑖𝑚𝑗))
17	11, 16	cfv 6380	. . . 4 class ((coe1‘(𝑖𝑚𝑗))‘𝑘)
18	6, 7, 10, 10, 17	cmpo 7215	. . 3 class (𝑖 ∈ dom dom 𝑚, 𝑗 ∈ dom dom 𝑚 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘))
19	2, 3, 4, 5, 18	cmpo 7215	. 2 class (𝑚 ∈ V, 𝑘 ∈ ℕ0 ↦ (𝑖 ∈ dom dom 𝑚, 𝑗 ∈ dom dom 𝑚 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)))
20	1, 19	wceq 1543	1 wff decompPMat = (𝑚 ∈ V, 𝑘 ∈ ℕ0 ↦ (𝑖 ∈ dom dom 𝑚, 𝑗 ∈ dom dom 𝑚 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)))

This definition is referenced by:  decpmatval0  21661  pmatcollpw3lem  21680