MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-decpmat Structured version   Visualization version   GIF version

Definition df-decpmat 20616
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
StepHypRef Expression
1 cdecpmat 20615 . 2 class decompPMat
2 vm . . 3 setvar 𝑚
3 vk . . 3 setvar 𝑘
4 cvv 3231 . . 3 class V
5 cn0 11330 . . 3 class 0
6 vi . . . 4 setvar 𝑖
7 vj . . . 4 setvar 𝑗
82cv 1522 . . . . . 6 class 𝑚
98cdm 5143 . . . . 5 class dom 𝑚
109cdm 5143 . . . 4 class dom dom 𝑚
113cv 1522 . . . . 5 class 𝑘
126cv 1522 . . . . . . 7 class 𝑖
137cv 1522 . . . . . . 7 class 𝑗
1412, 13, 8co 6690 . . . . . 6 class (𝑖𝑚𝑗)
15 cco1 19596 . . . . . 6 class coe1
1614, 15cfv 5926 . . . . 5 class (coe1‘(𝑖𝑚𝑗))
1711, 16cfv 5926 . . . 4 class ((coe1‘(𝑖𝑚𝑗))‘𝑘)
186, 7, 10, 10, 17cmpt2 6692 . . 3 class (𝑖 ∈ dom dom 𝑚, 𝑗 ∈ dom dom 𝑚 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘))
192, 3, 4, 5, 18cmpt2 6692 . 2 class (𝑚 ∈ V, 𝑘 ∈ ℕ0 ↦ (𝑖 ∈ dom dom 𝑚, 𝑗 ∈ dom dom 𝑚 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)))
201, 19wceq 1523 1 wff decompPMat = (𝑚 ∈ V, 𝑘 ∈ ℕ0 ↦ (𝑖 ∈ dom dom 𝑚, 𝑗 ∈ dom dom 𝑚 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)))
Colors of variables: wff setvar class
This definition is referenced by:  decpmatval0  20617  pmatcollpw3lem  20636
  Copyright terms: Public domain W3C validator