Home | Metamath
Proof Explorer Theorem List (p. 221 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mat2pmatghm 22001 | The transformation of matrices into polynomial matrices is an additive group homomorphism. (Contributed by AV, 28-Oct-2019.) (Proof shortened by AV, 28-Nov-2019.) |
β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π» = (BaseβπΆ) β β’ ((π β Fin β§ π β Ring) β π β (π΄ GrpHom πΆ)) | ||
Theorem | mat2pmatmul 22002* | The transformation of matrices into polynomial matrices preserves the multiplication. (Contributed by AV, 29-Oct-2019.) (Proof shortened by AV, 28-Nov-2019.) |
β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π» = (BaseβπΆ) β β’ ((π β Fin β§ π β CRing) β βπ₯ β π΅ βπ¦ β π΅ (πβ(π₯(.rβπ΄)π¦)) = ((πβπ₯)(.rβπΆ)(πβπ¦))) | ||
Theorem | mat2pmat1 22003 | The transformation of the identity matrix results in the identity polynomial matrix. (Contributed by AV, 29-Oct-2019.) |
β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π» = (BaseβπΆ) β β’ ((π β Fin β§ π β Ring) β (πβ(1rβπ΄)) = (1rβπΆ)) | ||
Theorem | mat2pmatmhm 22004 | The transformation of matrices into polynomial matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 29-Oct-2019.) |
β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π» = (BaseβπΆ) β β’ ((π β Fin β§ π β CRing) β π β ((mulGrpβπ΄) MndHom (mulGrpβπΆ))) | ||
Theorem | mat2pmatrhm 22005 | The transformation of matrices into polynomial matrices is a ring homomorphism. (Contributed by AV, 29-Oct-2019.) |
β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π» = (BaseβπΆ) β β’ ((π β Fin β§ π β CRing) β π β (π΄ RingHom πΆ)) | ||
Theorem | mat2pmatlin 22006 | The transformation of matrices into polynomial matrices is "linear", analogous to lmhmlin 20419. Since π΄ and πΆ have different scalar rings, π cannot be a left module homomorphism as defined in df-lmhm 20406, see lmhmsca 20414. (Contributed by AV, 13-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.) |
β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π» = (BaseβπΆ) & β’ πΎ = (Baseβπ ) & β’ π = (algScβπ) & β’ Β· = ( Β·π βπ΄) & β’ Γ = ( Β·π βπΆ) β β’ (((π β Fin β§ π β CRing) β§ (π β πΎ β§ π β π΅)) β (πβ(π Β· π)) = ((πβπ) Γ (πβπ))) | ||
Theorem | 0mat2pmat 22007 | The transformed zero matrix is the zero polynomial matrix. (Contributed by AV, 5-Aug-2019.) (Proof shortened by AV, 19-Nov-2019.) |
β’ π = (π matToPolyMat π ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβ(π Mat π )) & β’ π = (0gβ(π Mat π)) β β’ ((π β Ring β§ π β Fin) β (πβ 0 ) = π) | ||
Theorem | idmatidpmat 22008 | The transformed identity matrix is the identity polynomial matrix. (Contributed by AV, 1-Aug-2019.) (Proof shortened by AV, 19-Nov-2019.) |
β’ π = (π matToPolyMat π ) & β’ π = (Poly1βπ ) & β’ 1 = (1rβ(π Mat π )) & β’ πΌ = (1rβ(π Mat π)) β β’ ((π β Ring β§ π β Fin) β (πβ 1 ) = πΌ) | ||
Theorem | d0mat2pmat 22009 | The transformed empty set as matrix of dimenson 0 is the empty set (i.e., the polynomial matrix of dimension 0). (Contributed by AV, 4-Aug-2019.) |
β’ (π β π β ((β matToPolyMat π )ββ ) = β ) | ||
Theorem | d1mat2pmat 22010 | The transformation of a matrix of dimenson 1. (Contributed by AV, 4-Aug-2019.) |
β’ π = (π matToPolyMat π ) & β’ π΅ = (Baseβ(π Mat π )) & β’ π = (Poly1βπ ) & β’ π = (algScβπ) β β’ ((π β π β§ (π = {π΄} β§ π΄ β π) β§ π β π΅) β (πβπ) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©}) | ||
Theorem | mat2pmatscmxcl 22011 | A transformed matrix multiplied with a power of the variable of a polynomial is a polynomial matrix. (Contributed by AV, 6-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.) |
β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ΄) & β’ π = (π matToPolyMat π ) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) β β’ (((π β Fin β§ π β Ring) β§ (π β πΎ β§ πΏ β β0)) β ((πΏ β π) β (πβπ)) β π΅) | ||
Theorem | m2cpm 22012 | The result of a matrix transformation is a constant polynomial matrix. (Contributed by AV, 18-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.) |
β’ π = (π ConstPolyMat π ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β (πβπ) β π) | ||
Theorem | m2cpmf 22013 | The matrix transformation is a function from the matrices to the constant polynomial matrices. (Contributed by AV, 18-Nov-2019.) |
β’ π = (π ConstPolyMat π ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) β β’ ((π β Fin β§ π β Ring) β π:π΅βΆπ) | ||
Theorem | m2cpmf1 22014 | The matrix transformation is a 1-1 function from the matrices to the constant polynomial matrices. (Contributed by AV, 18-Nov-2019.) |
β’ π = (π ConstPolyMat π ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) β β’ ((π β Fin β§ π β Ring) β π:π΅β1-1βπ) | ||
Theorem | m2cpmghm 22015 | The transformation of matrices into constant polynomial matrices is an additive group homomorphism. (Contributed by AV, 18-Nov-2019.) |
β’ π = (π ConstPolyMat π ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π = (πΆ βΎs π) β β’ ((π β Fin β§ π β Ring) β π β (π΄ GrpHom π)) | ||
Theorem | m2cpmmhm 22016 | The transformation of matrices into constant polynomial matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 18-Nov-2019.) |
β’ π = (π ConstPolyMat π ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π = (πΆ βΎs π) β β’ ((π β Fin β§ π β CRing) β π β ((mulGrpβπ΄) MndHom (mulGrpβπ))) | ||
Theorem | m2cpmrhm 22017 | The transformation of matrices into constant polynomial matrices is a ring homomorphism. (Contributed by AV, 18-Nov-2019.) |
β’ π = (π ConstPolyMat π ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π = (πΆ βΎs π) β β’ ((π β Fin β§ π β CRing) β π β (π΄ RingHom π)) | ||
Theorem | m2pmfzmap 22018 | The transformed values of a (finite) mapping of integers to matrices. (Contributed by AV, 4-Nov-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (π matToPolyMat π ) β β’ (((π β Fin β§ π β Ring β§ π β β0) β§ (π β (π΅ βm (0...π)) β§ πΌ β (0...π))) β (πβ(πβπΌ)) β (Baseβπ)) | ||
Theorem | m2pmfzgsumcl 22019* | Closure of the sum of scaled transformed matrices. (Contributed by AV, 4-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (π matToPolyMat π ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β0 β§ π β (π΅ βm (0...π )))) β (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))) β (Baseβπ)) | ||
Theorem | cpm2mfval 22020* | Value of the inverse matrix transformation. (Contributed by AV, 14-Dec-2019.) |
β’ πΌ = (π cPolyMatToMat π ) & β’ π = (π ConstPolyMat π ) β β’ ((π β Fin β§ π β π) β πΌ = (π β π β¦ (π₯ β π, π¦ β π β¦ ((coe1β(π₯ππ¦))β0)))) | ||
Theorem | cpm2mval 22021* | The result of an inverse matrix transformation. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.) |
β’ πΌ = (π cPolyMatToMat π ) & β’ π = (π ConstPolyMat π ) β β’ ((π β Fin β§ π β π β§ π β π) β (πΌβπ) = (π₯ β π, π¦ β π β¦ ((coe1β(π₯ππ¦))β0))) | ||
Theorem | cpm2mvalel 22022 | A (matrix) element of the result of an inverse matrix transformation. (Contributed by AV, 14-Dec-2019.) |
β’ πΌ = (π cPolyMatToMat π ) & β’ π = (π ConstPolyMat π ) β β’ (((π β Fin β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (π(πΌβπ)π) = ((coe1β(πππ))β0)) | ||
Theorem | cpm2mf 22023 | The inverse matrix transformation is a function from the constant polynomial matrices to the matrices over the base ring of the polynomials. (Contributed by AV, 24-Nov-2019.) (Revised by AV, 15-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ΄) & β’ π = (π ConstPolyMat π ) & β’ πΌ = (π cPolyMatToMat π ) β β’ ((π β Fin β§ π β Ring) β πΌ:πβΆπΎ) | ||
Theorem | m2cpminvid 22024 | The inverse transformation applied to the transformation of a matrix over a ring R results in the matrix itself. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 13-Dec-2019.) |
β’ πΌ = (π cPolyMatToMat π ) & β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ΄) & β’ π = (π matToPolyMat π ) β β’ ((π β Fin β§ π β Ring β§ π β πΎ) β (πΌβ(πβπ)) = π) | ||
Theorem | m2cpminvid2lem 22025* | Lemma for m2cpminvid2 22026. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.) |
β’ π = (π ConstPolyMat π ) & β’ π = (Poly1βπ ) β β’ (((π β Fin β§ π β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β βπ β β0 ((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ)) | ||
Theorem | m2cpminvid2 22026 | The transformation applied to the inverse transformation of a constant polynomial matrix over the ring π results in the matrix itself. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.) |
β’ π = (π ConstPolyMat π ) & β’ πΌ = (π cPolyMatToMat π ) & β’ π = (π matToPolyMat π ) β β’ ((π β Fin β§ π β Ring β§ π β π) β (πβ(πΌβπ)) = π) | ||
Theorem | m2cpmfo 22027 | The matrix transformation is a function from the matrices onto the constant polynomial matrices. (Contributed by AV, 19-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.) |
β’ π = (π ConstPolyMat π ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ΄) β β’ ((π β Fin β§ π β Ring) β π:πΎβontoβπ) | ||
Theorem | m2cpmf1o 22028 | The matrix transformation is a 1-1 function from the matrices onto the constant polynomial matrices. (Contributed by AV, 19-Nov-2019.) |
β’ π = (π ConstPolyMat π ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ΄) β β’ ((π β Fin β§ π β Ring) β π:πΎβ1-1-ontoβπ) | ||
Theorem | m2cpmrngiso 22029 | The transformation of matrices into constant polynomial matrices is a ring isomorphism. (Contributed by AV, 19-Nov-2019.) |
β’ π = (π ConstPolyMat π ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π = (πΆ βΎs π) β β’ ((π β Fin β§ π β CRing) β π β (π΄ RingIso π)) | ||
Theorem | matcpmric 22030 | The ring of matrices over a commutative ring is isomorphic to the ring of scalar matrices over the same ring. (Contributed by AV, 30-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π = (π ConstPolyMat π ) & β’ π = (πΆ βΎs π) β β’ ((π β Fin β§ π β CRing) β π΄ βπ π) | ||
Theorem | m2cpminv 22031 | The inverse matrix transformation is a 1-1 function from the constant polynomial matrices onto the matrices over the base ring of the polynomials. (Contributed by AV, 27-Nov-2019.) (Revised by AV, 15-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ΄) & β’ π = (π ConstPolyMat π ) & β’ πΌ = (π cPolyMatToMat π ) & β’ π = (π matToPolyMat π ) β β’ ((π β Fin β§ π β Ring) β (πΌ:πβ1-1-ontoβπΎ β§ β‘πΌ = π)) | ||
Theorem | m2cpminv0 22032 | The inverse matrix transformation applied to the zero polynomial matrix results in the zero of the matrices over the base ring of the polynomials. (Contributed by AV, 24-Nov-2019.) (Revised by AV, 15-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ πΌ = (π cPolyMatToMat π ) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ 0 = (0gβπ΄) & β’ π = (0gβπΆ) β β’ ((π β Fin β§ π β Ring) β (πΌβπ) = 0 ) | ||
In this section, the decomposition of polynomial matrices into (polynomial) multiples of constant (polynomial) matrices is prepared by collecting the coefficients of a polynomial matrix which belong to the same power of the polynomial variable. Such a collection is given by the function decompPMat (see df-decpmat 22034), which maps a polynomial matrix π to a constant matrix consisting of the coefficients of the scaled monomials ((πβπ) β (π β π)), i.e. the coefficients belonging to the k-th power of the polynomial variable π, of each entry in the polynomial matrix π. The resulting decomposition is provided by Theorem pmatcollpw 22052. | ||
Syntax | cdecpmat 22033 | Extend class notation to include the decomposition of polynomial matrices. |
class decompPMat | ||
Definition | df-decpmat 22034* | 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.) |
β’ decompPMat = (π β V, π β β0 β¦ (π β dom dom π, π β dom dom π β¦ ((coe1β(πππ))βπ))) | ||
Theorem | decpmatval0 22035* | The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power, most general version. (Contributed by AV, 2-Dec-2019.) |
β’ ((π β π β§ πΎ β β0) β (π decompPMat πΎ) = (π β dom dom π, π β dom dom π β¦ ((coe1β(πππ))βπΎ))) | ||
Theorem | decpmatval 22036* | 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.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) β β’ ((π β π΅ β§ πΎ β β0) β (π decompPMat πΎ) = (π β π, π β π β¦ ((coe1β(πππ))βπΎ))) | ||
Theorem | decpmate 22037 | An entry of the matrix consisting of the coefficients in the entries of a polynomial matrix is the corresponding coefficient in the polynomial entry of the given matrix. (Contributed by AV, 28-Sep-2019.) (Revised by AV, 2-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) β β’ (((π β π β§ π β π΅ β§ πΎ β β0) β§ (πΌ β π β§ π½ β π)) β (πΌ(π decompPMat πΎ)π½) = ((coe1β(πΌππ½))βπΎ)) | ||
Theorem | decpmatcl 22038 | Closure of the decomposition of a polynomial matrix: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power is a matrix. (Contributed by AV, 28-Sep-2019.) (Revised by AV, 2-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ π΄ = (π Mat π ) & β’ π· = (Baseβπ΄) β β’ ((π β π β§ π β π΅ β§ πΎ β β0) β (π decompPMat πΎ) β π·) | ||
Theorem | decpmataa0 22039* | The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power is 0 for almost all powers. (Contributed by AV, 3-Nov-2019.) (Revised by AV, 3-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ π΄ = (π Mat π ) & β’ 0 = (0gβπ΄) β β’ ((π β Ring β§ π β π΅) β βπ β β0 βπ₯ β β0 (π < π₯ β (π decompPMat π₯) = 0 )) | ||
Theorem | decpmatfsupp 22040* | The mapping to the matrices consisting of the coefficients in the polynomial entries of a given matrix for the same power is finitely supported. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 3-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ π΄ = (π Mat π ) & β’ 0 = (0gβπ΄) β β’ ((π β Ring β§ π β π΅) β (π β β0 β¦ (π decompPMat π)) finSupp 0 ) | ||
Theorem | decpmatid 22041 | The matrix consisting of the coefficients in the polynomial entries of the identity matrix is an identity or a zero matrix. (Contributed by AV, 28-Sep-2019.) (Revised by AV, 2-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ πΌ = (1rβπΆ) & β’ π΄ = (π Mat π ) & β’ 0 = (0gβπ΄) & β’ 1 = (1rβπ΄) β β’ ((π β Fin β§ π β Ring β§ πΎ β β0) β (πΌ decompPMat πΎ) = if(πΎ = 0, 1 , 0 )) | ||
Theorem | decpmatmullem 22042* | Lemma for decpmatmul 22043. (Contributed by AV, 20-Oct-2019.) (Revised by AV, 3-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) β β’ (((π β Fin β§ π β Ring) β§ (π β π΅ β§ π β π΅) β§ (πΌ β π β§ π½ β π β§ πΎ β β0)) β (πΌ((π(.rβπΆ)π) decompPMat πΎ)π½) = (π Ξ£g (π‘ β π β¦ (π Ξ£g (π β (0...πΎ) β¦ (((coe1β(πΌππ‘))βπ)(.rβπ )((coe1β(π‘ππ½))β(πΎ β π)))))))) | ||
Theorem | decpmatmul 22043* | The matrix consisting of the coefficients in the polynomial entries of the product of two polynomial matrices is a sum of products of the matrices consisting of the coefficients in the polynomial entries of the polynomial matrices for the same power. (Contributed by AV, 21-Oct-2019.) (Revised by AV, 3-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ π΄ = (π Mat π ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β ((π(.rβπΆ)π) decompPMat πΎ) = (π΄ Ξ£g (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π)))))) | ||
Theorem | decpmatmulsumfsupp 22044* | Lemma 0 for pm2mpmhm 22091. (Contributed by AV, 21-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ π΄ = (π Mat π ) & β’ Β· = (.rβπ΄) & β’ 0 = (0gβπ΄) β β’ (((π β Fin β§ π β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β β0 β¦ (π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π) Β· (π¦ decompPMat (π β π)))))) finSupp 0 ) | ||
Theorem | pmatcollpw1lem1 22045* | Lemma 1 for pmatcollpw1 22047. (Contributed by AV, 28-Sep-2019.) (Revised by AV, 3-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ Γ = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) β β’ (((π β Fin β§ π β Ring β§ π β π΅) β§ πΌ β π β§ π½ β π) β (π β β0 β¦ ((πΌ(π decompPMat π)π½) Γ (π β π))) finSupp (0gβπ)) | ||
Theorem | pmatcollpw1lem2 22046* | Lemma 2 for pmatcollpw1 22047: An entry of a polynomial matrix is the sum of the entries of the matrix consisting of the coefficients in the entries of the polynomial matrix multiplied with the corresponding power of the variable. (Contributed by AV, 25-Sep-2019.) (Revised by AV, 3-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ Γ = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) β β’ (((π β Fin β§ π β Ring β§ π β π΅) β§ (π β π β§ π β π)) β (πππ) = (π Ξ£g (π β β0 β¦ ((π(π decompPMat π)π) Γ (π β π))))) | ||
Theorem | pmatcollpw1 22047* | Write a polynomial matrix as a matrix of sums of scaled monomials. (Contributed by AV, 29-Sep-2019.) (Revised by AV, 3-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ Γ = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β π = (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π(π decompPMat π)π) Γ (π β π)))))) | ||
Theorem | pmatcollpw2lem 22048* | Lemma for pmatcollpw2 22049. (Contributed by AV, 3-Oct-2019.) (Revised by AV, 3-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ Γ = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β (π β β0 β¦ (π β π, π β π β¦ ((π(π decompPMat π)π) Γ (π β π)))) finSupp (0gβπΆ)) | ||
Theorem | pmatcollpw2 22049* | Write a polynomial matrix as a sum of matrices whose entries are products of variable powers and constant polynomials collecting like powers. (Contributed by AV, 3-Oct-2019.) (Revised by AV, 3-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ Γ = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β π = (πΆ Ξ£g (π β β0 β¦ (π β π, π β π β¦ ((π(π decompPMat π)π) Γ (π β π)))))) | ||
Theorem | monmatcollpw 22050 | The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix having scaled monomials with the same power as entries is the matrix of the coefficients of the monomials or a zero matrix. Generalization of decpmatid 22041 (but requires π to be commutative!). (Contributed by AV, 11-Nov-2019.) (Revised by AV, 4-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ΄) & β’ 0 = (0gβπ΄) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπΆ) & β’ π = (π matToPolyMat π ) β β’ (((π β Fin β§ π β CRing) β§ (π β πΎ β§ πΏ β β0 β§ πΌ β β0)) β (((πΏ β π) Β· (πβπ)) decompPMat πΌ) = if(πΌ = πΏ, π, 0 )) | ||
Theorem | pmatcollpwlem 22051 | Lemma for pmatcollpw 22052. (Contributed by AV, 26-Oct-2019.) (Revised by AV, 4-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) β β’ ((((π β Fin β§ π β CRing β§ π β π΅) β§ π β β0) β§ π β π β§ π β π) β ((π(π decompPMat π)π)( Β·π βπ)(π β π)) = (π((π β π) β (πβ(π decompPMat π)))π)) | ||
Theorem | pmatcollpw 22052* | Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 26-Oct-2019.) (Revised by AV, 4-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β π = (πΆ Ξ£g (π β β0 β¦ ((π β π) β (πβ(π decompPMat π)))))) | ||
Theorem | pmatcollpwfi 22053* | Write a polynomial matrix (over a commutative ring) as a finite sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 4-Nov-2019.) (Revised by AV, 4-Dec-2019.) (Proof shortened by AV, 3-Jul-2022.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β βπ β β0 π = (πΆ Ξ£g (π β (0...π ) β¦ ((π β π) β (πβ(π decompPMat π)))))) | ||
Theorem | pmatcollpw3lem 22054* | Lemma for pmatcollpw3 22055 and pmatcollpw3fi 22056: Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 8-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π· = (Baseβπ΄) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (πΌ β β0 β§ πΌ β β )) β (π = (πΆ Ξ£g (π β πΌ β¦ ((π β π) β (πβ(π decompPMat π))))) β βπ β (π· βm πΌ)π = (πΆ Ξ£g (π β πΌ β¦ ((π β π) β (πβ(πβπ))))))) | ||
Theorem | pmatcollpw3 22055* | Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 27-Oct-2019.) (Revised by AV, 4-Dec-2019.) (Proof shortened by AV, 8-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π· = (Baseβπ΄) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β βπ β (π· βm β0)π = (πΆ Ξ£g (π β β0 β¦ ((π β π) β (πβ(πβπ)))))) | ||
Theorem | pmatcollpw3fi 22056* | Write a polynomial matrix (over a commutative ring) as a finite sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 4-Nov-2019.) (Revised by AV, 4-Dec-2019.) (Proof shortened by AV, 8-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π· = (Baseβπ΄) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β βπ β β0 βπ β (π· βm (0...π ))π = (πΆ Ξ£g (π β (0...π ) β¦ ((π β π) β (πβ(πβπ)))))) | ||
Theorem | pmatcollpw3fi1lem1 22057* | Lemma 1 for pmatcollpw3fi1 22059. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π· = (Baseβπ΄) & β’ 0 = (0gβπ΄) & β’ π» = (π β (0...1) β¦ if(π = 0, (πΊβ0), 0 )) β β’ (((π β Fin β§ π β Ring) β§ πΊ β (π· βm {0}) β§ π = (πΆ Ξ£g (π β {0} β¦ ((π β π) β (πβ(πΊβπ)))))) β π = (πΆ Ξ£g (π β (0...1) β¦ ((π β π) β (πβ(π»βπ)))))) | ||
Theorem | pmatcollpw3fi1lem2 22058* | Lemma 2 for pmatcollpw3fi1 22059. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π· = (Baseβπ΄) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β (βπ β (π· βm {0})π = (πΆ Ξ£g (π β {0} β¦ ((π β π) β (πβ(πβπ))))) β βπ β β βπ β (π· βm (0...π ))π = (πΆ Ξ£g (π β (0...π ) β¦ ((π β π) β (πβ(πβπ))))))) | ||
Theorem | pmatcollpw3fi1 22059* | Write a polynomial matrix (over a commutative ring) as a finite sum of (at least two) products of variable powers and constant matrices with scalar entries. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π· = (Baseβπ΄) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β βπ β β βπ β (π· βm (0...π ))π = (πΆ Ξ£g (π β (0...π ) β¦ ((π β π) β (πβ(πβπ)))))) | ||
Theorem | pmatcollpwscmatlem1 22060 | Lemma 1 for pmatcollpwscmat 22062. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π· = (Baseβπ΄) & β’ π = (algScβπ) & β’ πΎ = (Baseβπ ) & β’ πΈ = (Baseβπ) & β’ π = (algScβπ) & β’ 1 = (1rβπΆ) & β’ π = (π β 1 ) β β’ ((((π β Fin β§ π β Ring) β§ (πΏ β β0 β§ π β πΈ)) β§ (π β π β§ π β π)) β (((coe1β(πππ))βπΏ)( Β·π βπ)(0(.gβ(mulGrpβπ))(var1βπ ))) = if(π = π, (πβ((coe1βπ)βπΏ)), (0gβπ))) | ||
Theorem | pmatcollpwscmatlem2 22061 | Lemma 2 for pmatcollpwscmat 22062. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π· = (Baseβπ΄) & β’ π = (algScβπ) & β’ πΎ = (Baseβπ ) & β’ πΈ = (Baseβπ) & β’ π = (algScβπ) & β’ 1 = (1rβπΆ) & β’ π = (π β 1 ) β β’ (((π β Fin β§ π β Ring) β§ (πΏ β β0 β§ π β πΈ)) β (πβ(π decompPMat πΏ)) = ((πβ((coe1βπ)βπΏ)) β 1 )) | ||
Theorem | pmatcollpwscmat 22062* | Write a scalar matrix over polynomials (over a commutative ring) as a sum of the product of variable powers and constant scalar matrices with scalar entries. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπΆ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ π΄ = (π Mat π ) & β’ π· = (Baseβπ΄) & β’ π = (algScβπ) & β’ πΎ = (Baseβπ ) & β’ πΈ = (Baseβπ) & β’ π = (algScβπ) & β’ 1 = (1rβπΆ) & β’ π = (π β 1 ) β β’ ((π β Fin β§ π β CRing β§ π β πΈ) β π = (πΆ Ξ£g (π β β0 β¦ ((π β π) β ((πβ((coe1βπ)βπ)) β 1 ))))) | ||
The main result of this section is Theorem pmmpric 22094, which shows that the
ring of polynomial matrices and the ring of polynomials having matrices as
coefficients (called "polynomials over matrices" in the following) are
isomorphic:
| ||
Syntax | cpm2mp 22063 | Extend class notation with the transformation of a polynomial matrix into a polynomial over matrices. |
class pMatToMatPoly | ||
Definition | df-pm2mp 22064* | Transformation of a polynomial matrix (over a ring) into a polynomial over matrices (over the same ring). (Contributed by AV, 5-Dec-2019.) |
β’ pMatToMatPoly = (π β Fin, π β V β¦ (π β (Baseβ(π Mat (Poly1βπ))) β¦ β¦(π Mat π) / πβ¦β¦(Poly1βπ) / πβ¦(π Ξ£g (π β β0 β¦ ((π decompPMat π)( Β·π βπ)(π(.gβ(mulGrpβπ))(var1βπ))))))) | ||
Theorem | pm2mpf1lem 22065* | Lemma for pm2mpf1 22070. (Contributed by AV, 14-Oct-2019.) (Revised by AV, 4-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) β β’ (((π β Fin β§ π β Ring) β§ (π β π΅ β§ πΎ β β0)) β ((coe1β(π Ξ£g (π β β0 β¦ ((π decompPMat π) β (π β π)))))βπΎ) = (π decompPMat πΎ)) | ||
Theorem | pm2mpval 22066* | Value of the transformation of a polynomial matrix into a polynomial over matrices. (Contributed by AV, 5-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β π) β π = (π β π΅ β¦ (π Ξ£g (π β β0 β¦ ((π decompPMat π) β (π β π)))))) | ||
Theorem | pm2mpfval 22067* | A polynomial matrix transformed into a polynomial over matrices. (Contributed by AV, 4-Oct-2019.) (Revised by AV, 5-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β π β§ π β π΅) β (πβπ) = (π Ξ£g (π β β0 β¦ ((π decompPMat π) β (π β π))))) | ||
Theorem | pm2mpcl 22068 | The transformation of polynomial matrices into polynomials over matrices maps polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 5-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) & β’ πΏ = (Baseβπ) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β (πβπ) β πΏ) | ||
Theorem | pm2mpf 22069 | The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 5-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) & β’ πΏ = (Baseβπ) β β’ ((π β Fin β§ π β Ring) β π:π΅βΆπΏ) | ||
Theorem | pm2mpf1 22070 | The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 14-Oct-2019.) (Revised by AV, 6-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) & β’ πΏ = (Baseβπ) β β’ ((π β Fin β§ π β Ring) β π:π΅β1-1βπΏ) | ||
Theorem | pm2mpcoe1 22071 | A coefficient of the polynomial over matrices which is the result of the transformation of a polynomial matrix is the matrix consisting of the coefficients in the polynomial entries of the polynomial matrix. (Contributed by AV, 20-Oct-2019.) (Revised by AV, 5-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ (((π β Fin β§ π β Ring) β§ (π β π΅ β§ πΎ β β0)) β ((coe1β(πβπ))βπΎ) = (π decompPMat πΎ)) | ||
Theorem | idpm2idmp 22072 | The transformation of the identity polynomial matrix into polynomials over matrices results in the identity of the polynomials over matrices. (Contributed by AV, 18-Oct-2019.) (Revised by AV, 5-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β (πβ(1rβπΆ)) = (1rβπ)) | ||
Theorem | mptcoe1matfsupp 22073* | The mapping extracting the entries of the coefficient matrices of a polynomial over matrices at a fixed position is finitely supported. (Contributed by AV, 6-Oct-2019.) (Proof shortened by AV, 23-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) β β’ (((π β Fin β§ π β Ring β§ π β πΏ) β§ πΌ β π β§ π½ β π) β (π β β0 β¦ (πΌ((coe1βπ)βπ)π½)) finSupp (0gβπ )) | ||
Theorem | mply1topmatcllem 22074* | Lemma for mply1topmatcl 22076. (Contributed by AV, 6-Oct-2019.) |
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) β β’ (((π β Fin β§ π β Ring β§ π β πΏ) β§ πΌ β π β§ π½ β π) β (π β β0 β¦ ((πΌ((coe1βπ)βπ)π½) Β· (ππΈπ))) finSupp (0gβπ)) | ||
Theorem | mply1topmatval 22075* | A polynomial over matrices transformed into a polynomial matrix. πΌ is the inverse function of the transformation π of polynomial matrices into polynomials over matrices: (πβ(πΌβπ)) = π) (see mp2pm2mp 22082). (Contributed by AV, 6-Oct-2019.) |
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) β β’ ((π β π β§ π β πΏ) β (πΌβπ) = (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) | ||
Theorem | mply1topmatcl 22076* | A polynomial over matrices transformed into a polynomial matrix is a polynomial matrix. (Contributed by AV, 6-Oct-2019.) |
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) β β’ ((π β Fin β§ π β Ring β§ π β πΏ) β (πΌβπ) β π΅) | ||
Theorem | mp2pm2mplem1 22077* | Lemma 1 for mp2pm2mp 22082. (Contributed by AV, 9-Oct-2019.) (Revised by AV, 5-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) β β’ ((π β Fin β§ π β Ring β§ π β πΏ) β (πΌβπ) = (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) | ||
Theorem | mp2pm2mplem2 22078* | Lemma 2 for mp2pm2mp 22082. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 5-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) β β’ ((π β Fin β§ π β Ring β§ π β πΏ) β (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ))))) β π΅) | ||
Theorem | mp2pm2mplem3 22079* | Lemma 3 for mp2pm2mp 22082. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 5-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) & β’ π = (Poly1βπ ) β β’ (((π β Fin β§ π β Ring β§ π β πΏ) β§ πΎ β β0) β ((πΌβπ) decompPMat πΎ) = (π β π, π β π β¦ ((coe1β(π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))βπΎ))) | ||
Theorem | mp2pm2mplem4 22080* | Lemma 4 for mp2pm2mp 22082. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) & β’ π = (Poly1βπ ) β β’ (((π β Fin β§ π β Ring β§ π β πΏ) β§ πΎ β β0) β ((πΌβπ) decompPMat πΎ) = ((coe1βπ)βπΎ)) | ||
Theorem | mp2pm2mplem5 22081* | Lemma 5 for mp2pm2mp 22082. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) & β’ π = (Poly1βπ ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) β β’ ((π β Fin β§ π β Ring β§ π β πΏ) β (π β β0 β¦ (((πΌβπ) decompPMat π) β (π β π))) finSupp (0gβπ)) | ||
Theorem | mp2pm2mp 22082* | A polynomial over matrices transformed into a polynomial matrix transformed back into the polynomial over matrices. (Contributed by AV, 12-Oct-2019.) |
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) & β’ π = (Poly1βπ ) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring β§ π β πΏ) β (πβ(πΌβπ)) = π) | ||
Theorem | pm2mpghmlem2 22083* | Lemma 2 for pm2mpghm 22087. (Contributed by AV, 15-Oct-2019.) (Revised by AV, 4-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β (π β β0 β¦ ((π decompPMat π) β (π β π))) finSupp (0gβπ)) | ||
Theorem | pm2mpghmlem1 22084 | Lemma 1 for pm2mpghm . (Contributed by AV, 15-Oct-2019.) (Revised by AV, 4-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) β β’ (((π β Fin β§ π β Ring β§ π β π΅) β§ πΎ β β0) β ((π decompPMat πΎ) β (πΎ β π)) β πΏ) | ||
Theorem | pm2mpfo 22085 | The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 6-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π:π΅βontoβπΏ) | ||
Theorem | pm2mpf1o 22086 | The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 14-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π:π΅β1-1-ontoβπΏ) | ||
Theorem | pm2mpghm 22087 | The transformation of polynomial matrices into polynomials over matrices is an additive group homomorphism. (Contributed by AV, 16-Oct-2019.) (Revised by AV, 6-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π β (πΆ GrpHom π)) | ||
Theorem | pm2mpgrpiso 22088 | The transformation of polynomial matrices into polynomials over matrices is an additive group isomorphism. (Contributed by AV, 17-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π β (πΆ GrpIso π)) | ||
Theorem | pm2mpmhmlem1 22089* | Lemma 1 for pm2mpmhm 22091. (Contributed by AV, 21-Oct-2019.) (Revised by AV, 6-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (π pMatToMatPoly π ) β β’ (((π β Fin β§ π β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β β0 β¦ ((π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) β (π β π))) finSupp (0gβπ)) | ||
Theorem | pm2mpmhmlem2 22090* | Lemma 2 for pm2mpmhm 22091. (Contributed by AV, 22-Oct-2019.) (Revised by AV, 6-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) & β’ π΅ = (BaseβπΆ) β β’ ((π β Fin β§ π β Ring) β βπ₯ β π΅ βπ¦ β π΅ (πβ(π₯(.rβπΆ)π¦)) = ((πβπ₯)(.rβπ)(πβπ¦))) | ||
Theorem | pm2mpmhm 22091 | The transformation of polynomial matrices into polynomials over matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 22-Oct-2019.) (Revised by AV, 6-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π β ((mulGrpβπΆ) MndHom (mulGrpβπ))) | ||
Theorem | pm2mprhm 22092 | The transformation of polynomial matrices into polynomials over matrices is a ring homomorphism. (Contributed by AV, 22-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π β (πΆ RingHom π)) | ||
Theorem | pm2mprngiso 22093 | The transformation of polynomial matrices into polynomials over matrices is a ring isomorphism. (Contributed by AV, 22-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π β (πΆ RingIso π)) | ||
Theorem | pmmpric 22094 | The ring of polynomial matrices over a ring is isomorphic to the ring of polynomials over matrices of the same dimension over the same ring. (Contributed by AV, 30-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) β β’ ((π β Fin β§ π β Ring) β πΆ βπ π) | ||
Theorem | monmat2matmon 22095 | The transformation of a polynomial matrix having scaled monomials with the same power as entries into a scaled monomial as a polynomial over matrices. (Contributed by AV, 11-Nov-2019.) (Revised by AV, 7-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ΄) & β’ π = (Poly1βπ΄) & β’ πΌ = (π pMatToMatPoly π ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπΆ) & β’ π = (π matToPolyMat π ) β β’ (((π β Fin β§ π β CRing) β§ (π β πΎ β§ πΏ β β0)) β (πΌβ((πΏπΈπ) Β· (πβπ))) = (π β (πΏ β π))) | ||
Theorem | pm2mp 22096* | The transformation of a sum of matrices having scaled monomials with the same power as entries into a sum of scaled monomials as a polynomial over matrices. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 7-Dec-2019.) |
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ΄) & β’ π = (Poly1βπ΄) & β’ πΌ = (π pMatToMatPoly π ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπΆ) & β’ π = (π matToPolyMat π ) β β’ (((π β Fin β§ π β CRing) β§ (π β (πΎ βm β0) β§ π finSupp (0gβπ΄))) β (πΌβ(πΆ Ξ£g (π β β0 β¦ ((ππΈπ) Β· (πβ(πβπ)))))) = (π Ξ£g (π β β0 β¦ ((πβπ) β (π β π))))) | ||
According to Wikipedia ("Characteristic polynomial", 31-Jul-2019, https://en.wikipedia.org/wiki/Characteristic_polynomial): "In linear algebra, the characteristic polynomial of a square matrix is a polynomial which is invariant under matrix similarity and has the eigenvalues as roots. It has the determinant and the trace of the matrix as coefficients.". Based on the definition of the characteristic polynomial of a square matrix (df-chpmat 22098) the eigenvalues and corresponding eigenvectors can be defined. | ||
The characteristic polynomial of a matrix π΄ is the determinant of the characteristic matrix of π΄: (π‘πΌ β π΄). | ||
Syntax | cchpmat 22097 | Extend class notation with the characteristic polynomial. |
class CharPlyMat | ||
Definition | df-chpmat 22098* | Define the characteristic polynomial of a square matrix. According to Wikipedia ("Characteristic polynomial", 31-Jul-2019, https://en.wikipedia.org/wiki/Characteristic_polynomial): "The characteristic polynomial of [an n x n matrix] A, denoted by pA(t), is the polynomial defined by pA ( t ) = det ( t I - A ) where I denotes the n-by-n identity matrix.". In addition, however, the underlying ring must be commutative, see definition in [Lang], p. 561: " Let k be a commutative ring ... Let M be any n x n matrix in k ... We define the characteristic polynomial PM(t) to be the determinant det ( t In - M ) where In is the unit n x n matrix." To be more precise, the matrices A and I on the right hand side are matrices with coefficients of a polynomial ring. Therefore, the original matrix A over a given commutative ring must be transformed into corresponding matrices over the polynomial ring over the given ring. (Contributed by AV, 2-Aug-2019.) |
β’ CharPlyMat = (π β Fin, π β V β¦ (π β (Baseβ(π Mat π)) β¦ ((π maDet (Poly1βπ))β(((var1βπ)( Β·π β(π Mat (Poly1βπ)))(1rβ(π Mat (Poly1βπ))))(-gβ(π Mat (Poly1βπ)))((π matToPolyMat π)βπ))))) | ||
Theorem | chmatcl 22099 | Closure of the characteristic matrix of a matrix. (Contributed by AV, 25-Oct-2019.) (Proof shortened by AV, 29-Nov-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ β = (-gβπ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π» = ((π Β· 1 ) β (πβπ)) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β π» β (Baseβπ)) | ||
Theorem | chmatval 22100 | The entries of the characteristic matrix of a matrix. (Contributed by AV, 2-Aug-2019.) (Proof shortened by AV, 10-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ β = (-gβπ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π» = ((π Β· 1 ) β (πβπ)) & β’ βΌ = (-gβπ) & β’ 0 = (0gβπ) β β’ (((π β Fin β§ π β Ring β§ π β π΅) β§ (πΌ β π β§ π½ β π)) β (πΌπ»π½) = if(πΌ = π½, (π βΌ (πΌ(πβπ)π½)), ( 0 βΌ (πΌ(πβπ)π½)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |