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

Definition df-decpmat 19718
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.)
Assertion
Ref Expression
df-decpmat  |- decompPMat  =  ( m  e.  _V , 
k  e.  NN0  |->  ( i  e.  dom  dom  m ,  j  e.  dom  dom  m  |->  ( (coe1 `  (
i m j ) ) `  k ) ) )
Distinct variable group:    i, j, k, m

Detailed syntax breakdown of Definition df-decpmat
StepHypRef Expression
1 cdecpmat 19717 . 2  class decompPMat
2 vm . . 3  setvar  m
3 vk . . 3  setvar  k
4 cvv 3087 . . 3  class  _V
5 cn0 10869 . . 3  class  NN0
6 vi . . . 4  setvar  i
7 vj . . . 4  setvar  j
82cv 1436 . . . . . 6  class  m
98cdm 4854 . . . . 5  class  dom  m
109cdm 4854 . . . 4  class  dom  dom  m
113cv 1436 . . . . 5  class  k
126cv 1436 . . . . . . 7  class  i
137cv 1436 . . . . . . 7  class  j
1412, 13, 8co 6305 . . . . . 6  class  ( i m j )
15 cco1 18706 . . . . . 6  class coe1
1614, 15cfv 5601 . . . . 5  class  (coe1 `  (
i m j ) )
1711, 16cfv 5601 . . . 4  class  ( (coe1 `  ( i m j ) ) `  k
)
186, 7, 10, 10, 17cmpt2 6307 . . 3  class  ( i  e.  dom  dom  m ,  j  e.  dom  dom  m  |->  ( (coe1 `  (
i m j ) ) `  k ) )
192, 3, 4, 5, 18cmpt2 6307 . 2  class  ( m  e.  _V ,  k  e.  NN0  |->  ( i  e.  dom  dom  m ,  j  e.  dom  dom  m  |->  ( (coe1 `  (
i m j ) ) `  k ) ) )
201, 19wceq 1437 1  wff decompPMat  =  ( m  e.  _V , 
k  e.  NN0  |->  ( i  e.  dom  dom  m ,  j  e.  dom  dom  m  |->  ( (coe1 `  (
i m j ) ) `  k ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  decpmatval0  19719  pmatcollpw3lem  19738
  Copyright terms: Public domain W3C validator