Metamath Proof Explorer


Theorem decpmatval

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power, general version for arbitrary matrices. (Contributed by AV, 28-Sep-2019) (Revised by AV, 2-Dec-2019)

Ref Expression
Hypotheses decpmatval.a A = N Mat R
decpmatval.b B = Base A
Assertion decpmatval M B K 0 M decompPMat K = i N , j N coe 1 i M j K

Proof

Step Hyp Ref Expression
1 decpmatval.a A = N Mat R
2 decpmatval.b B = Base A
3 decpmatval0 M B K 0 M decompPMat K = i dom dom M , j dom dom M coe 1 i M j K
4 eqid Base R = Base R
5 1 4 2 matbas2i M B M Base R N × N
6 elmapi M Base R N × N M : N × N Base R
7 fdm M : N × N Base R dom M = N × N
8 7 dmeqd M : N × N Base R dom dom M = dom N × N
9 dmxpid dom N × N = N
10 8 9 eqtrdi M : N × N Base R dom dom M = N
11 5 6 10 3syl M B dom dom M = N
12 11 adantr M B K 0 dom dom M = N
13 eqidd M B K 0 coe 1 i M j K = coe 1 i M j K
14 12 12 13 mpoeq123dv M B K 0 i dom dom M , j dom dom M coe 1 i M j K = i N , j N coe 1 i M j K
15 3 14 eqtrd M B K 0 M decompPMat K = i N , j N coe 1 i M j K