P. 196 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19501-19600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cpmatpmat 19501	A constant polynomial matrix is a polynomial matrix. (Contributed by AV, 16-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. V /\ M e. S ) -> M e. B )
Theorem	cpmatel 19502*	Property of a constant polynomial matrix. (Contributed by AV, 15-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( M e. S <-> A. i e. N A. j e. N A. k e. NN ( (coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )
Theorem	cpmatelimp 19503*	Implication of a set being a constant polynomial matrix. (Contributed by AV, 18-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( M e. S -> ( M e. B /\ A. i e. N A. j e. N A. k e. NN ( (coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) ) )
Theorem	cpmatel2 19504*	Another property of a constant polynomial matrix. (Contributed by AV, 16-Nov-2019.) (Proof shortened by AV, 27-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- K = ( Base ` R )   &    |- A = (algSc ` P )   =>    |- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( M e. S <-> A. i e. N A. j e. N E. k e. K ( i M j ) = ( A ` k ) ) )
Theorem	cpmatelimp2 19505*	Another implication of a set being a constant polynomial matrix. (Contributed by AV, 17-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- K = ( Base ` R )   &    |- A = (algSc ` P )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( M e. S -> ( M e. B /\ A. i e. N A. j e. N E. k e. K ( i M j ) = ( A ` k ) ) ) )
Theorem	1elcpmat 19506	The identity of the ring of all polynomial matrices over the ring R is a constant polynomial matrix. (Contributed by AV, 16-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) e. S )
Theorem	cpmatacl 19507*	The set of all constant polynomial matrices over a ring R is closed under addition. (Contributed by AV, 17-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( +g ` C ) y ) e. S )
Theorem	cpmatinvcl 19508*	The set of all constant polynomial matrices over a ring R is closed under inversion. (Contributed by AV, 17-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> A. x e. S ( ( invg ` C ) ` x ) e. S )
Theorem	cpmatmcllem 19509*	Lemma for cpmatmcl 19510. (Contributed by AV, 18-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> A. i e. N A. j e. N A. c e. NN ( (coe1 ` ( P gsumg ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) )
Theorem	cpmatmcl 19510*	The set of all constant polynomial matrices over a ring R is closed under multiplication. (Contributed by AV, 18-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( .r ` C ) y ) e. S )
Theorem	cpmatsubgpmat 19511	The set of all constant polynomial matrices over a ring R is an additive subgroup of the ring of all polynomial matrices over the ring R. (Contributed by AV, 15-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> S e. (SubGrp ` C ) )
Theorem	cpmatsrgpmat 19512	The set of all constant polynomial matrices over a ring R is a subring of the ring of all polynomial matrices over the ring R. (Contributed by AV, 18-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> S e. (SubRing ` C ) )
Theorem	0elcpmat 19513	The zero of the ring of all polynomial matrices over the ring R is a constant polynomial matrix. (Contributed by AV, 27-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` C ) e. S )
Theorem	mat2pmatfval 19514*	Value of the matrix transformation. (Contributed by AV, 31-Jul-2019.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- S = (algSc ` P )   =>    |- ( ( N e. Fin /\ R e. V ) -> T = ( m e. B |-> ( x e. N , y e. N |-> ( S ` ( x m y ) ) ) ) )
Theorem	mat2pmatval 19515*	The result of a matrix transformation. (Contributed by AV, 31-Jul-2019.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- S = (algSc ` P )   =>    |- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( T ` M ) = ( x e. N , y e. N |-> ( S ` ( x M y ) ) ) )
Theorem	mat2pmatvalel 19516	A (matrix) element of the result of a matrix transformation. (Contributed by AV, 31-Jul-2019.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- S = (algSc ` P )   =>    |- ( ( ( N e. Fin /\ R e. V /\ M e. B ) /\ ( X e. N /\ Y e. N ) ) -> ( X ( T ` M ) Y ) = ( S ` ( X M Y ) ) )
Theorem	mat2pmatbas 19517	The result of a matrix transformation is a polynomial matrix. (Contributed by AV, 1-Aug-2019.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   =>    |- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` C ) )
Theorem	mat2pmatbas0 19518	The result of a matrix transformation is a polynomial matrix. (Contributed by AV, 27-Oct-2019.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- H = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. H )
Theorem	mat2pmatf 19519	The matrix transformation is a function from the matrices to the polynomial matrices. (Contributed by AV, 27-Oct-2019.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- H = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> T : B --> H )
Theorem	mat2pmatf1 19520	The matrix transformation is a 1-1 function from the matrices to the polynomial matrices. (Contributed by AV, 28-Oct-2019.) (Proof shortened by AV, 27-Nov-2019.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- H = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-> H )
Theorem	mat2pmatghm 19521	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.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- H = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom C ) )
Theorem	mat2pmatmul 19522*	The transformation of matrices into polynomial matrices preserves the multiplication. (Contributed by AV, 29-Oct-2019.) (Proof shortened by AV, 28-Nov-2019.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- H = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. CRing ) -> A. x e. B A. y e. B ( T ` ( x ( .r ` A ) y ) ) = ( ( T ` x ) ( .r ` C ) ( T ` y ) ) )
Theorem	mat2pmat1 19523	The transformation of the identity matrix results in the identity polynomial matrix. (Contributed by AV, 29-Oct-2019.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- H = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( T ` ( 1r ` A ) ) = ( 1r ` C ) )
Theorem	mat2pmatmhm 19524	The transformation of matrices into polynomial matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 29-Oct-2019.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- H = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. CRing ) -> T e. ( (mulGrp ` A ) MndHom (mulGrp ` C ) ) )
Theorem	mat2pmatrhm 19525	The transformation of matrices into polynomial matrices is a ring homomorphism. (Contributed by AV, 29-Oct-2019.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- H = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom C ) )
Theorem	mat2pmatlin 19526	The transformation of matrices into polynomial matrices is "linear", analogous to lmhmlin 17999. Since A and C have different scalar rings, T cannot be a left module homomorphism as defined in df-lmhm 17986, see lmhmsca 17994. (Contributed by AV, 13-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.)
|- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- H = ( Base ` C )   &    |- K = ( Base ` R )   &    |- S = (algSc ` P )   &    |- .x. = ( .s ` A )   &    |- .X. = ( .s ` C )   =>    |- ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( T ` ( X .x. Y ) ) = ( ( S ` X ) .X. ( T ` Y ) ) )
Theorem	0mat2pmat 19527	The transformed zero matrix is the zero polynomial matrix. (Contributed by AV, 5-Aug-2019.) (Proof shortened by AV, 19-Nov-2019.)
|- T = ( N matToPolyMat R )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` ( N Mat R ) )   &    |- Z = ( 0g ` ( N Mat P ) )   =>    |- ( ( R e. Ring /\ N e. Fin ) -> ( T ` .0. ) = Z )
Theorem	idmatidpmat 19528	The transformed identity matrix is the identity polynomial matrix. (Contributed by AV, 1-Aug-2019.) (Proof shortened by AV, 19-Nov-2019.)
|- T = ( N matToPolyMat R )   &    |- P = (Poly1 ` R )   &    |- .1. = ( 1r ` ( N Mat R ) )   &    |- I = ( 1r ` ( N Mat P ) )   =>    |- ( ( R e. Ring /\ N e. Fin ) -> ( T ` .1. ) = I )
Theorem	d0mat2pmat 19529	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.)
|- ( R e. V -> ( ( (/) matToPolyMat R ) ` (/) ) = (/) )
Theorem	d1mat2pmat 19530	The transformation of a matrix of dimenson 1. (Contributed by AV, 4-Aug-2019.)
|- T = ( N matToPolyMat R )   &    |- B = ( Base ` ( N Mat R ) )   &    |- P = (Poly1 ` R )   &    |- S = (algSc ` P )   =>    |- ( ( R e. V /\ ( N = { A } /\ A e. V ) /\ M e. B ) -> ( T ` M ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } )
Theorem	mat2pmatscmxcl 19531	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.)
|- A = ( N Mat R )   &    |- K = ( Base ` A )   &    |- T = ( N matToPolyMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> ( ( L .^ X ) .* ( T ` M ) ) e. B )
Theorem	m2cpm 19532	The result of a matrix transformation is a constant polynomial matrix. (Contributed by AV, 18-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   =>    |- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. S )
Theorem	m2cpmf 19533	The matrix transformation is a function from the matrices to the constant polynomial matrices. (Contributed by AV, 18-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> T : B --> S )
Theorem	m2cpmf1 19534	The matrix transformation is a 1-1 function from the matrices to the constant polynomial matrices. (Contributed by AV, 18-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-> S )
Theorem	m2cpmghm 19535	The transformation of matrices into constant polynomial matrices is an additive group homomorphism. (Contributed by AV, 18-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- U = ( C ↾s S )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom U ) )
Theorem	m2cpmmhm 19536	The transformation of matrices into constant polynomial matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 18-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- U = ( C ↾s S )   =>    |- ( ( N e. Fin /\ R e. CRing ) -> T e. ( (mulGrp ` A ) MndHom (mulGrp ` U ) ) )
Theorem	m2cpmrhm 19537	The transformation of matrices into constant polynomial matrices is a ring homomorphism. (Contributed by AV, 18-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- U = ( C ↾s S )   =>    |- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom U ) )
Theorem	m2pmfzmap 19538	The transformed values of a (finite) mapping of integers to matrices. (Contributed by AV, 4-Nov-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- Y = ( N Mat P )   &    |- T = ( N matToPolyMat R )   =>    |- ( ( ( N e. Fin /\ R e. Ring /\ S e. NN0 ) /\ ( b e. ( B ^m ( 0 ... S ) ) /\ I e. ( 0 ... S ) ) ) -> ( T ` ( b ` I ) ) e. ( Base ` Y ) )
Theorem	m2pmfzgsumcl 19539*	Closure of the sum of scaled transformed matrices. (Contributed by AV, 4-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- Y = ( N Mat P )   &    |- T = ( N matToPolyMat R )   &    |- X = (var1 ` R )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- .x. = ( .s ` Y )   =>    |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) )
Theorem	cpm2mfval 19540*	Value of the inverse matrix transformation. (Contributed by AV, 14-Dec-2019.)
|- I = ( N cPolyMatToMat R )   &    |- S = ( N ConstPolyMat R )   =>    |- ( ( N e. Fin /\ R e. V ) -> I = ( m e. S |-> ( x e. N , y e. N |-> ( (coe1 ` ( x m y ) ) ` 0 ) ) ) )
Theorem	cpm2mval 19541*	The result of an inverse matrix transformation. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.)
|- I = ( N cPolyMatToMat R )   &    |- S = ( N ConstPolyMat R )   =>    |- ( ( N e. Fin /\ R e. V /\ M e. S ) -> ( I ` M ) = ( x e. N , y e. N |-> ( (coe1 ` ( x M y ) ) ` 0 ) ) )
Theorem	cpm2mvalel 19542	A (matrix) element of the result of an inverse matrix transformation. (Contributed by AV, 14-Dec-2019.)
|- I = ( N cPolyMatToMat R )   &    |- S = ( N ConstPolyMat R )   =>    |- ( ( ( N e. Fin /\ R e. V /\ M e. S ) /\ ( X e. N /\ Y e. N ) ) -> ( X ( I ` M ) Y ) = ( (coe1 ` ( X M Y ) ) ` 0 ) )
Theorem	cpm2mf 19543	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.)
|- A = ( N Mat R )   &    |- K = ( Base ` A )   &    |- S = ( N ConstPolyMat R )   &    |- I = ( N cPolyMatToMat R )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> I : S --> K )
Theorem	m2cpminvid 19544	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.)
|- I = ( N cPolyMatToMat R )   &    |- A = ( N Mat R )   &    |- K = ( Base ` A )   &    |- T = ( N matToPolyMat R )   =>    |- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( I ` ( T ` M ) ) = M )
Theorem	m2cpminvid2lem 19545*	Lemma for m2cpminvid2 19546. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.)
|- S = ( N ConstPolyMat R )   &    |- P = (Poly1 ` R )   =>    |- ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> A. n e. NN0 ( (coe1 ` ( (algSc ` P ) ` ( (coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( (coe1 ` ( x M y ) ) ` n ) )
Theorem	m2cpminvid2 19546	The transformation applied to the inverse transformation of a constant polynomial matrix over the ring R results in the matrix itself. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.)
|- S = ( N ConstPolyMat R )   &    |- I = ( N cPolyMatToMat R )   &    |- T = ( N matToPolyMat R )   =>    |- ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( T ` ( I ` M ) ) = M )
Theorem	m2cpmfo 19547	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.)
|- S = ( N ConstPolyMat R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- K = ( Base ` A )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> T : K -onto-> S )
Theorem	m2cpmf1o 19548	The matrix transformation is a 1-1 function from the matrices onto the constant polynomial matrices. (Contributed by AV, 19-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- K = ( Base ` A )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> T : K -1-1-onto-> S )
Theorem	m2cpmrngiso 19549	The transformation of matrices into constant polynomial matrices is a ring isomorphism. (Contributed by AV, 19-Nov-2019.)
|- S = ( N ConstPolyMat R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- K = ( Base ` A )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- U = ( C ↾s S )   =>    |- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingIso U ) )
Theorem	matcpmric 19550	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.)
|- A = ( N Mat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- S = ( N ConstPolyMat R )   &    |- U = ( C ↾s S )   =>    |- ( ( N e. Fin /\ R e. CRing ) -> A ~=r U )
Theorem	m2cpminv 19551	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.)
|- A = ( N Mat R )   &    |- K = ( Base ` A )   &    |- S = ( N ConstPolyMat R )   &    |- I = ( N cPolyMatToMat R )   &    |- T = ( N matToPolyMat R )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( I : S -1-1-onto-> K /\ `' I = T ) )
Theorem	m2cpminv0 19552	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.)
|- A = ( N Mat R )   &    |- I = ( N cPolyMatToMat R )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- .0. = ( 0g ` A )   &    |- Z = ( 0g ` C )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( I ` Z ) = .0. )
11.4.3  Collecting coefficients of polynomial matrices 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 functiondecompPMat ( see df-decpmat 19554), which maps a polynomial matrix M to a constant matrix consisting of the coefficients of the scaled monomials ( ( c ` k ) .* ( k .^ X ) ), i.e. the coefficients belonging to the k-th power of the polynomial variable X, of each entry in the polynomial matrix M. The resulting decomposition is provided by theorem pmatcollpw 19572.
Syntax	cdecpmat 19553	Extend class notation to include the decomposition of polynomial matrices.
class decompPMat
Definition	df-decpmat 19554*	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.)
|- decompPMat = ( m e. _V , k e. NN0 |-> ( i e. dom dom m , j e. dom dom m |-> ( (coe1 ` ( i m j ) ) ` k ) ) )
Theorem	decpmatval0 19555*	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.)
|- ( ( M e. V /\ K e. NN0 ) -> ( M decompPMat K ) = ( i e. dom dom M , j e. dom dom M |-> ( (coe1 ` ( i M j ) ) ` K ) ) )
Theorem	decpmatval 19556*	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   =>    |- ( ( M e. B /\ K e. NN0 ) -> ( M decompPMat K ) = ( i e. N , j e. N |-> ( (coe1 ` ( i M j ) ) ` K ) ) )
Theorem	decpmate 19557	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   =>    |- ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ ( I e. N /\ J e. N ) ) -> ( I ( M decompPMat K ) J ) = ( (coe1 ` ( I M J ) ) ` K ) )
Theorem	decpmatcl 19558	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- A = ( N Mat R )   &    |- D = ( Base ` A )   =>    |- ( ( R e. V /\ M e. B /\ K e. NN0 ) -> ( M decompPMat K ) e. D )
Theorem	decpmataa0 19559*	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- A = ( N Mat R )   &    |- .0. = ( 0g ` A )   =>    |- ( ( R e. Ring /\ M e. B ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( M decompPMat x ) = .0. ) )
Theorem	decpmatfsupp 19560*	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- A = ( N Mat R )   &    |- .0. = ( 0g ` A )   =>    |- ( ( R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( M decompPMat k ) ) finSupp .0. )
Theorem	decpmatid 19561	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- I = ( 1r ` C )   &    |- A = ( N Mat R )   &    |- .0. = ( 0g ` A )   &    |- .1. = ( 1r ` A )   =>    |- ( ( N e. Fin /\ R e. Ring /\ K e. NN0 ) -> ( I decompPMat K ) = if ( K = 0 , .1. , .0. ) )
Theorem	decpmatmullem 19562*	Lemma for decpmatmul 19563. (Contributed by AV, 20-Oct-2019.) (Revised by AV, 3-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ W e. B ) /\ ( I e. N /\ J e. N /\ K e. NN0 ) ) -> ( I ( ( U ( .r ` C ) W ) decompPMat K ) J ) = ( R gsumg ( t e. N |-> ( R gsumg ( l e. ( 0 ... K ) |-> ( ( (coe1 ` ( I U t ) ) ` l ) ( .r ` R ) ( (coe1 ` ( t W J ) ) ` ( K - l ) ) ) ) ) ) ) )
Theorem	decpmatmul 19563*	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- A = ( N Mat R )   =>    |- ( ( R e. Ring /\ ( U e. B /\ W e. B ) /\ K e. NN0 ) -> ( ( U ( .r ` C ) W ) decompPMat K ) = ( A gsumg ( k e. ( 0 ... K ) |-> ( ( U decompPMat k ) ( .r ` A ) ( W decompPMat ( K - k ) ) ) ) ) )
Theorem	decpmatmulsumfsupp 19564*	Lemma 0 for pm2mpmhm 19611. (Contributed by AV, 21-Oct-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- A = ( N Mat R )   &    |- .x. = ( .r ` A )   &    |- .0. = ( 0g ` A )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( l e. NN0 |-> ( A gsumg ( k e. ( 0 ... l ) |-> ( ( x decompPMat k ) .x. ( y decompPMat ( l - k ) ) ) ) ) ) finSupp .0. )
Theorem	pmatcollpw1lem1 19565*	Lemma 1 for pmatcollpw1 19567. (Contributed by AV, 28-Sep-2019.) (Revised by AV, 3-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .X. = ( .s ` P )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   =>    |- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ I e. N /\ J e. N ) -> ( n e. NN0 |-> ( ( I ( M decompPMat n ) J ) .X. ( n .^ X ) ) ) finSupp ( 0g ` P ) )
Theorem	pmatcollpw1lem2 19566*	Lemma 2 for pmatcollpw1 19567: 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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .X. = ( .s ` P )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   =>    |- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( a M b ) = ( P gsumg ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) ) )
Theorem	pmatcollpw1 19567*	Write a polynomial matrix as a matrix of sums of scaled monomials. (Contributed by AV, 29-Sep-2019.) (Revised by AV, 3-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .X. = ( .s ` P )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   =>    |- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> M = ( i e. N , j e. N |-> ( P gsumg ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) )
Theorem	pmatcollpw2lem 19568*	Lemma for pmatcollpw2 19569. (Contributed by AV, 3-Oct-2019.) (Revised by AV, 3-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .X. = ( .s ` P )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   =>    |- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) finSupp ( 0g ` C ) )
Theorem	pmatcollpw2 19569*	Write a polynomial matrix as 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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .X. = ( .s ` P )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   =>    |- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> M = ( C gsumg ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) )
Theorem	monmatcollpw 19570	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 19561 (but requires R to be commutative!). (Contributed by AV, 11-Nov-2019.) (Revised by AV, 4-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- A = ( N Mat R )   &    |- K = ( Base ` A )   &    |- .0. = ( 0g ` A )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- .x. = ( .s ` C )   &    |- T = ( N matToPolyMat R )   =>    |- ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ I e. NN0 ) ) -> ( ( ( L .^ X ) .x. ( T ` M ) ) decompPMat I ) = if ( I = L , M , .0. ) )
Theorem	pmatcollpwlem 19571	Lemma for pmatcollpw 19572. (Contributed by AV, 26-Oct-2019.) (Revised by AV, 4-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- T = ( N matToPolyMat R )   =>    |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) = ( a ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) b ) )
Theorem	pmatcollpw 19572*	Write a polynomial matrix (over a commutative ring) as sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 26-Oct-2019.) (Revised by AV, 4-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- T = ( N matToPolyMat R )   =>    |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> M = ( C gsumg ( n e. NN0 |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )
Theorem	pmatcollpwfi 19573*	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- T = ( N matToPolyMat R )   =>    |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN0 M = ( C gsumg ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )
Theorem	pmatcollpw3lem 19574*	Lemma for pmatcollpw3 19575 and pmatcollpw3fi 19576: Write a polynomial matrix (over a commutative ring) as sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 8-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- D = ( Base ` A )   =>    |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( M = ( C gsumg ( n e. I |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) -> E. f e. ( D ^m I ) M = ( C gsumg ( n e. I |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
Theorem	pmatcollpw3 19575*	Write a polynomial matrix (over a commutative ring) as 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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- D = ( Base ` A )   =>    |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. f e. ( D ^m NN0 ) M = ( C gsumg ( n e. NN0 |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )
Theorem	pmatcollpw3fi 19576*	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- D = ( Base ` A )   =>    |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN0 E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsumg ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )
Theorem	pmatcollpw3fi1lem1 19577*	Lemma 1 for pmatcollpw3fi1 19579. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- D = ( Base ` A )   &    |- .0. = ( 0g ` A )   &    |- H = ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( G ` 0 ) , .0. ) )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) /\ M = ( C gsumg ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) ) -> M = ( C gsumg ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) )
Theorem	pmatcollpw3fi1lem2 19578*	Lemma 2 for pmatcollpw3fi1 19579. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- D = ( Base ` A )   =>    |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. f e. ( D ^m { 0 } ) M = ( C gsumg ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsumg ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
Theorem	pmatcollpw3fi1 19579*	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- D = ( Base ` A )   =>    |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsumg ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )
Theorem	pmatcollpwscmatlem1 19580	Lemma 1 for pmatcollpwscmat 19582. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- D = ( Base ` A )   &    |- U = (algSc ` P )   &    |- K = ( Base ` R )   &    |- E = ( Base ` P )   &    |- S = (algSc ` P )   &    |- .1. = ( 1r ` C )   &    |- M = ( Q .* .1. )   =>    |- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( ( (coe1 ` ( a M b ) ) ` L ) ( .s ` P ) ( 0 (.g ` (mulGrp ` P ) ) (var1 ` R ) ) ) = if ( a = b , ( U ` ( (coe1 ` Q ) ` L ) ) , ( 0g ` P ) ) )
Theorem	pmatcollpwscmatlem2 19581	Lemma 2 for pmatcollpwscmat 19582. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- D = ( Base ` A )   &    |- U = (algSc ` P )   &    |- K = ( Base ` R )   &    |- E = ( Base ` P )   &    |- S = (algSc ` P )   &    |- .1. = ( 1r ` C )   &    |- M = ( Q .* .1. )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( T ` ( M decompPMat L ) ) = ( ( U ` ( (coe1 ` Q ) ` L ) ) .* .1. ) )
Theorem	pmatcollpwscmat 19582*	Write a scalar matrix over polynomials (over a commutative ring) as 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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` C )   &    |- .^ = (.g ` (mulGrp ` P ) )   &    |- X = (var1 ` R )   &    |- T = ( N matToPolyMat R )   &    |- A = ( N Mat R )   &    |- D = ( Base ` A )   &    |- U = (algSc ` P )   &    |- K = ( Base ` R )   &    |- E = ( Base ` P )   &    |- S = (algSc ` P )   &    |- .1. = ( 1r ` C )   &    |- M = ( Q .* .1. )   =>    |- ( ( N e. Fin /\ R e. CRing /\ Q e. E ) -> M = ( C gsumg ( n e. NN0 |-> ( ( n .^ X ) .* ( ( U ` ( (coe1 ` Q ) ` n ) ) .* .1. ) ) ) ) )
11.4.4  Ring isomorphism between polynomial matrices and polynomials over matrices The main result of this section is theorem pmmpric 19614, 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: (Poly1 ` ( N Mat R ) ) ~= ( N Mat (Poly1 ` R ) ) Or in a more common notation: ( N Mat (Poly1 ` R ) ) corresponds to M(n, R[t]), the ring of n x n polynomial matrices over the ring R. (Poly1 ` ( N Mat R ) ) corresponds to M(n, R)[t], the polynomial ring over the ring of n x n matrices with entries in ring R. T = ( m e. B |-> ( Q gsumg ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) ) with B = ( Base ` ( N Mat (Poly1 ` R ) ) ) and ( m decompPMat k ) = ( i e. N , j e. N |-> ( (coe1 ( i m j ) ) k ) ) ) is an isomorphism between these rings: T : B -1-1-onto-> L with L = ( Base ` (Poly1 ` ( N Mat R ) ) ) (see pm2mpf1o 19606 and pm2mprngiso 19613), and I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 p ) k ) j ) .x. ( k E Y ) ) ) ) ) ) is the corresponding inverse function: ( T ` ( I ` O ) ) = O ) (see mp2pm2mp 19602). In this section, the following conventions are mostly used: R is a (unital) ring (see df-ring 17518) P = (Poly1 ` R ) is the polynomial algebra over (the ring) R (see df-ply1 18539) K = ( Base ` P ) is its base set (see df-base 14844) Y = (var1 ` R ) is its variable (see df-vr1 18538) .x. = ( .s ` P ) is its scalar multiplication (see df-vsca 14924 or lmodvscl 17847) E = (.g ` (mulGrp ` P ) ) is its exponentiation (see df-mulg 16382) A = ( N Mat R ) is the algebra of N x N matrices over (the ring) R (see df-mat 19200) C = ( N Mat P ) is the algebra of N x N matrices over (the polynomial ring) P. B = ( Base ` C ) is its base set M e. B is a concrete polynomial matrix Q = (Poly1 ` A ) is the polynomial algebra over (the matrix ring) A. L = ( Base ` Q ) is its base set O e. L is a concrete polynomial with matrix coefficients X = (var1 ` A ) is its variable .* = ( .s ` Q ) is its scalar multiplication .^ = (.g ` (mulGrp ` Q ) ) is its exponentiation
Syntax	cpm2mp 19583	Extend class notation with the transformation of a polynomial matrix into a polynomial over matrices.
class pMatToMatPoly
Definition	df-pm2mp 19584*	Transformation of a polynomial matrix (over a ring) into a polynomial over matrices (over the same ring). (Contributed by AV, 5-Dec-2019.)
|- pMatToMatPoly = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat (Poly1 ` r ) ) ) |-> [_ ( n Mat r ) / a ]_ [_ (Poly1 ` a ) / q ]_ ( q gsumg ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k (.g ` (mulGrp ` q ) ) (var1 ` a ) ) ) ) ) ) )
Theorem	pm2mpf1lem 19585*	Lemma for pm2mpf1 19590. (Contributed by AV, 14-Oct-2019.) (Revised by AV, 4-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` Q )   &    |- .^ = (.g ` (mulGrp ` Q ) )   &    |- X = (var1 ` A )   &    |- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( U e. B /\ K e. NN0 ) ) -> ( (coe1 ` ( Q gsumg ( k e. NN0 |-> ( ( U decompPMat k ) .* ( k .^ X ) ) ) ) ) ` K ) = ( U decompPMat K ) )
Theorem	pm2mpval 19586*	Value of the transformation of a polynomial matrix into a polynomial over matrices. (Contributed by AV, 5-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` Q )   &    |- .^ = (.g ` (mulGrp ` Q ) )   &    |- X = (var1 ` A )   &    |- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- T = ( N pMatToMatPoly R )   =>    |- ( ( N e. Fin /\ R e. V ) -> T = ( m e. B |-> ( Q gsumg ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) ) )
Theorem	pm2mpfval 19587*	A polynomial matrix transformed into a polynomial over matrices. (Contributed by AV, 4-Oct-2019.) (Revised by AV, 5-Dec-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` Q )   &    |- .^ = (.g ` (mulGrp ` Q ) )   &    |- X = (var1 ` A )   &    |- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- T = ( N pMatToMatPoly R )   =>    |- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( T ` M ) = ( Q gsumg ( k e. NN0 |-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) ) )
Theorem	pm2mpcl 19588	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` Q )   &    |- .^ = (.g ` (mulGrp ` Q ) )   &    |- X = (var1 ` A )   &    |- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- T = ( N pMatToMatPoly R )   &    |- L = ( Base ` Q )   =>    |- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. L )
Theorem	pm2mpf 19589	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` Q )   &    |- .^ = (.g ` (mulGrp ` Q ) )   &    |- X = (var1 ` A )   &    |- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- T = ( N pMatToMatPoly R )   &    |- L = ( Base ` Q )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> T : B --> L )
Theorem	pm2mpf1 19590	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` Q )   &    |- .^ = (.g ` (mulGrp ` Q ) )   &    |- X = (var1 ` A )   &    |- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- T = ( N pMatToMatPoly R )   &    |- L = ( Base ` Q )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-> L )
Theorem	pm2mpcoe1 19591	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` Q )   &    |- .^ = (.g ` (mulGrp ` Q ) )   &    |- X = (var1 ` A )   &    |- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- T = ( N pMatToMatPoly R )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> ( (coe1 ` ( T ` M ) ) ` K ) = ( M decompPMat K ) )
Theorem	idpm2idmp 19592	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.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   &    |- .* = ( .s ` Q )   &    |- .^ = (.g ` (mulGrp ` Q ) )   &    |- X = (var1 ` A )   &    |- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- T = ( N pMatToMatPoly R )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( T ` ( 1r ` C ) ) = ( 1r ` Q ) )
Theorem	mptcoe1matfsupp 19593*	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.)
|- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- L = ( Base ` Q )   =>    |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( k e. NN0 |-> ( I ( (coe1 ` O ) ` k ) J ) ) finSupp ( 0g ` R ) )
Theorem	mply1topmatcllem 19594*	Lemma for mply1topmatcl 19596. (Contributed by AV, 6-Oct-2019.)
|- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- L = ( Base ` Q )   &    |- P = (Poly1 ` R )   &    |- .x. = ( .s ` P )   &    |- E = (.g ` (mulGrp ` P ) )   &    |- Y = (var1 ` R )   =>    |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( k e. NN0 |-> ( ( I ( (coe1 ` O ) ` k ) J ) .x. ( k E Y ) ) ) finSupp ( 0g ` P ) )
Theorem	mply1topmatval 19595*	A polynomial over matrices transformed into a polynomial matrix. I is the inverse function of the transformation T of polynomial matrices into polynomials over matrices: ( T ` ( I ` O ) ) = O ) (see mp2pm2mp 19602). (Contributed by AV, 6-Oct-2019.)
|- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- L = ( Base ` Q )   &    |- P = (Poly1 ` R )   &    |- .x. = ( .s ` P )   &    |- E = (.g ` (mulGrp ` P ) )   &    |- Y = (var1 ` R )   &    |- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )   =>    |- ( ( N e. V /\ O e. L ) -> ( I ` O ) = ( i e. N , j e. N |-> ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
Theorem	mply1topmatcl 19596*	A polynomial over matrices transformed into a polynomial matrix is a polynomial matrix. (Contributed by AV, 6-Oct-2019.)
|- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- L = ( Base ` Q )   &    |- P = (Poly1 ` R )   &    |- .x. = ( .s ` P )   &    |- E = (.g ` (mulGrp ` P ) )   &    |- Y = (var1 ` R )   &    |- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( I ` O ) e. B )
Theorem	mp2pm2mplem1 19597*	Lemma 1 for mp2pm2mp 19602. (Contributed by AV, 9-Oct-2019.) (Revised by AV, 5-Dec-2019.)
|- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- L = ( Base ` Q )   &    |- .x. = ( .s ` P )   &    |- E = (.g ` (mulGrp ` P ) )   &    |- Y = (var1 ` R )   &    |- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )   =>    |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( I ` O ) = ( i e. N , j e. N |-> ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
Theorem	mp2pm2mplem2 19598*	Lemma 2 for mp2pm2mp 19602. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 5-Dec-2019.)
|- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- L = ( Base ` Q )   &    |- .x. = ( .s ` P )   &    |- E = (.g ` (mulGrp ` P ) )   &    |- Y = (var1 ` R )   &    |- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )   &    |- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- B = ( Base ` C )   =>    |- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( i e. N , j e. N |-> ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) e. B )
Theorem	mp2pm2mplem3 19599*	Lemma 3 for mp2pm2mp 19602. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 5-Dec-2019.)
|- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- L = ( Base ` Q )   &    |- .x. = ( .s ` P )   &    |- E = (.g ` (mulGrp ` P ) )   &    |- Y = (var1 ` R )   &    |- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )   &    |- P = (Poly1 ` R )   =>    |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( I ` O ) decompPMat K ) = ( i e. N , j e. N |-> ( (coe1 ` ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ` K ) ) )
Theorem	mp2pm2mplem4 19600*	Lemma 4 for mp2pm2mp 19602. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.)
|- A = ( N Mat R )   &    |- Q = (Poly1 ` A )   &    |- L = ( Base ` Q )   &    |- .x. = ( .s ` P )   &    |- E = (.g ` (mulGrp ` P ) )   &    |- Y = (var1 ` R )   &    |- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsumg ( k e. NN0 |-> ( ( i ( (coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )   &    |- P = (Poly1 ` R )   =>    |- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ K e. NN0 ) -> ( ( I ` O ) decompPMat K ) = ( (coe1 ` O ) ` K ) )