Metamath Proof Explorer

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 ∈ V , k ∈ ℕ 0 ⟼ i ∈ dom ⁡ dom ⁡ m , j ∈ dom ⁡ dom ⁡ m ⟼ coe 1 ⁡ i m j ⁡ k

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdecpmat class decompPMat
1 vm setvar m
2 cvv class V
3 vk setvar k
4 cn0 class ℕ 0
5 vi setvar i
6 1 cv setvar m
7 6 cdm class dom ⁡ m
8 7 cdm class dom ⁡ dom ⁡ m
9 vj setvar j
10 cco1 class coe 1
11 5 cv setvar i
12 9 cv setvar j
13 11 12 6 co class i m j
14 13 10 cfv class coe 1 ⁡ i m j
15 3 cv setvar k
16 15 14 cfv class coe 1 ⁡ i m j ⁡ k
17 5 9 8 8 16 cmpo class i ∈ dom ⁡ dom ⁡ m , j ∈ dom ⁡ dom ⁡ m ⟼ coe 1 ⁡ i m j ⁡ k
18 1 3 2 4 17 cmpo class m ∈ V , k ∈ ℕ 0 ⟼ i ∈ dom ⁡ dom ⁡ m , j ∈ dom ⁡ dom ⁡ m ⟼ coe 1 ⁡ i m j ⁡ k
19 0 18 wceq wff decompPMat = m ∈ V , k ∈ ℕ 0 ⟼ i ∈ dom ⁡ dom ⁡ m , j ∈ dom ⁡ dom ⁡ m ⟼ coe 1 ⁡ i m j ⁡ k