P. 227 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22601-22700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cramerlem2 22601*	Lemma 2 for cramer 22604. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ∀𝑧 ∈ 𝑉 ((𝑋 · 𝑧) = 𝑌 → 𝑧 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋)))))
Theorem	cramerlem3 22602*	Lemma 3 for cramer 22604. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌))
Theorem	cramer0 22603*	Special case of Cramer's rule for 0-dimensional matrices/vectors. (Contributed by AV, 28-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌))
Theorem	cramer 22604*	Cramer's rule. According to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule: "[Cramer's rule] ... expresses the [unique] solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations." If it is assumed that a (unique) solution exists, it can be obtained by Cramer's rule (see also cramerimp 22599). On the other hand, if a vector can be constructed by Cramer's rule, it is a solution of the system of linear equations, so at least one solution exists. The uniqueness is ensured by considering only systems of linear equations whose matrix has a unit (of the underlying ring) as determinant, see matunit 22591 or slesolinv 22593. For fields as underlying rings, this requirement is equivalent to the determinant not being 0. Theorem 4.4 in [Lang] p. 513. This is Metamath 100 proof #97. (Contributed by Alexander van der Vekens, 21-Feb-2019.) (Revised by Alexander van der Vekens, 1-Mar-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ (𝑋 · 𝑍) = 𝑌))
11.6  Polynomial matrices A polynomial matrix or matrix of polynomials is a matrix whose elements are univariate (or multivariate) polynomials. See Wikipedia "Polynomial matrix" https://en.wikipedia.org/wiki/Polynomial_matrix (18-Nov-2019). In this section, only square matrices whose elements are univariate polynomials are considered. Usually, the ring of such matrices, the ring of n x n matrices over the polynomial ring over a ring 𝑅, is denoted by M(n, R[t]). The elements of this ring are called "polynomial matrices (over the ring 𝑅)" in the following. In Metamath notation, this ring is defined by (𝑁 Mat (Poly1‘𝑅)), usually represented by the class variable 𝐶 (or 𝑌, if 𝐶 is already occupied): 𝐶 = (𝑁 Mat 𝑃) with 𝑃 = (Poly1‘𝑅).
11.6.1  Basic properties
Theorem	pmatring 22605	The set of polynomial matrices over a ring is a ring. (Contributed by AV, 6-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring)
Theorem	pmatlmod 22606	The set of polynomial matrices over a ring is a left module. (Contributed by AV, 6-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ LMod)
Theorem	pmatassa 22607	The set of polynomial matrices over a commutative ring is an associative algebra. (Contributed by AV, 16-Jun-2024.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ AssAlg)
Theorem	pmat0op 22608*	The zero polynomial matrix over a ring represented as operation. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 0 = (0g‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 0 ))
Theorem	pmat1op 22609*	The identity polynomial matrix over a ring represented as operation. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 1 = (1r‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, 1 , 0 )))
Theorem	pmat1ovd 22610	Entries of the identity polynomial matrix over a ring, deduction form. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 1 = (1r‘𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑁)    &   ⊢ 𝑈 = (1r‘𝐶)    ⇒   ⊢ (𝜑 → (𝐼𝑈𝐽) = if(𝐼 = 𝐽, 1 , 0 ))
Theorem	pmat0opsc 22611*	The zero polynomial matrix over a ring represented as operation with "lifted scalars" (i.e. elements of the ring underlying the polynomial ring embedded into the polynomial ring by the scalar injection/algebra scalar lifting function algSc). (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝐴‘ 0 )))
Theorem	pmat1opsc 22612*	The identity polynomial matrix over a ring represented as operation with "lifted scalars". (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝐴‘ 1 ), (𝐴‘ 0 ))))
Theorem	pmat1ovscd 22613	Entries of the identity polynomial matrix over a ring represented with "lifted scalars", deduction form. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑁)    &   ⊢ 𝑈 = (1r‘𝐶)    ⇒   ⊢ (𝜑 → (𝐼𝑈𝐽) = if(𝐼 = 𝐽, (𝐴‘ 1 ), (𝐴‘ 0 )))
Theorem	pmatcoe1fsupp 22614*	For a polynomial matrix there is an upper bound for the coefficients of all the polynomials being not 0. (Contributed by AV, 3-Oct-2019.) (Proof shortened by AV, 28-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 ))
Theorem	1pmatscmul 22615	The scalar product of the identity polynomial matrix with a polynomial is a polynomial matrix. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐸 = (Base‘𝑃)    &   ⊢ ∗ = ( ·𝑠 ‘𝐶)    &   ⊢ 1 = (1r‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸) → (𝑄 ∗ 1 ) ∈ 𝐵)
11.6.2  Constant polynomial matrices A constant polynomial matrix is a polynomial matrix whose elements are constant polynomials, i.e., polynomials with no indeterminates. Constant polynomials are obtained by "lifting" a "scalar" (i.e. an element of the underlying ring) into the polynomial ring/algebra by a "scalar injection", i.e., applying the "algebra scalar injection function" algSc (see df-ascl 21790) to a scalar 𝐴 ∈ 𝑅: ((algSc‘𝑃)‘𝐴). Analogously, constant polynomial matrices (over the ring 𝑅) are obtained by "lifting" matrices over the ring 𝑅 by the function matToPolyMat (see df-mat2pmat 22620), called "matrix transformation" in the following. In this section it is shown that the set 𝑆 = (𝑁 ConstPolyMat 𝑅) of constant polynomial 𝑁 x 𝑁 matrices over the ring 𝑅 is a subring of the ring of polynomial 𝑁 x 𝑁 matrices over the ring 𝑅 (cpmatsrgpmat 22634) and that 𝑇 = (𝑁 matToPolyMat 𝑅) is a ring isomorphism from the ring of matrices over a ring 𝑅 onto the ring of constant polynomial matrices over the ring 𝑅 (see m2cpmrngiso 22671). Thus, the ring of matrices over a commutative ring is isomorphic to the ring of scalar matrices over the same ring, see matcpmric 22672. Finally, 𝐼 = (𝑁 cPolyMatToMat 𝑅), the transformation of a constant polynomial matrix into a matrix, is the inverse function of the matrix transformation 𝑇 = (𝑁 matToPolyMat 𝑅), see m2cpminv 22673.
Syntax	ccpmat 22616	Extend class notation with the set of all constant polynomial matrices.
class ConstPolyMat
Syntax	cmat2pmat 22617	Extend class notation with the transformation of a matrix into a matrix of polynomials.
class matToPolyMat
Syntax	ccpmat2mat 22618	Extend class notation with the transformation of a constant polynomial matrix into a matrix.
class cPolyMatToMat
Definition	df-cpmat 22619*	The set of all constant polynomial matrices, which are all matrices whose entries are constant polynomials (or "scalar polynomials", see ply1sclf 22197). (Contributed by AV, 15-Nov-2019.)
⊢ ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)})
Definition	df-mat2pmat 22620*	Transformation of a matrix (over a ring) into a matrix over the corresponding polynomial ring. (Contributed by AV, 31-Jul-2019.)
⊢ matToPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))))
Definition	df-cpmat2mat 22621*	Transformation of a constant polynomial matrix (over a ring) into a matrix over the corresponding ring. Since this function is the inverse function of matToPolyMat, see m2cpminv 22673, it is also called "inverse matrix transformation" in the following. (Contributed by AV, 14-Dec-2019.)
⊢ cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
Theorem	cpmat 22622*	Value of the constructor of the set of all constant polynomial matrices, i.e. the set of all 𝑁 x 𝑁 matrices of polynomials over a ring 𝑅. (Contributed by AV, 15-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑆 = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)})
Theorem	cpmatpmat 22623	A constant polynomial matrix is a polynomial matrix. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) → 𝑀 ∈ 𝐵)
Theorem	cpmatel 22624*	Property of a constant polynomial matrix. (Contributed by AV, 15-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑀 ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅)))
Theorem	cpmatelimp 22625*	Implication of a set being a constant polynomial matrix. (Contributed by AV, 18-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝑆 → (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅))))
Theorem	cpmatel2 22626*	Another property of a constant polynomial matrix. (Contributed by AV, 16-Nov-2019.) (Proof shortened by AV, 27-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑀 ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑘 ∈ 𝐾 (𝑖𝑀𝑗) = (𝐴‘𝑘)))
Theorem	cpmatelimp2 22627*	Another implication of a set being a constant polynomial matrix. (Contributed by AV, 17-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝑆 → (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑘 ∈ 𝐾 (𝑖𝑀𝑗) = (𝐴‘𝑘))))
Theorem	1elcpmat 22628	The identity of the ring of all polynomial matrices over the ring 𝑅 is a constant polynomial matrix. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r‘𝐶) ∈ 𝑆)
Theorem	cpmatacl 22629*	The set of all constant polynomial matrices over a ring 𝑅 is closed under addition. (Contributed by AV, 17-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐶)𝑦) ∈ 𝑆)
Theorem	cpmatinvcl 22630*	The set of all constant polynomial matrices over a ring 𝑅 is closed under inversion. (Contributed by AV, 17-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝑆 ((invg‘𝐶)‘𝑥) ∈ 𝑆)
Theorem	cpmatmcllem 22631*	Lemma for cpmatmcl 22632. (Contributed by AV, 18-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑐 ∈ ℕ ((coe1‘(𝑃 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑥𝑘)(.r‘𝑃)(𝑘𝑦𝑗)))))‘𝑐) = (0g‘𝑅))
Theorem	cpmatmcl 22632*	The set of all constant polynomial matrices over a ring 𝑅 is closed under multiplication. (Contributed by AV, 18-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝐶)𝑦) ∈ 𝑆)
Theorem	cpmatsubgpmat 22633	The set of all constant polynomial matrices over a ring 𝑅 is an additive subgroup of the ring of all polynomial matrices over the ring 𝑅. (Contributed by AV, 15-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ (SubGrp‘𝐶))
Theorem	cpmatsrgpmat 22634	The set of all constant polynomial matrices over a ring 𝑅 is a subring of the ring of all polynomial matrices over the ring 𝑅. (Contributed by AV, 18-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ (SubRing‘𝐶))
Theorem	0elcpmat 22635	The zero of the ring of all polynomial matrices over the ring 𝑅 is a constant polynomial matrix. (Contributed by AV, 27-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐶) ∈ 𝑆)
Theorem	mat2pmatfval 22636*	Value of the matrix transformation. (Contributed by AV, 31-Jul-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦)))))
Theorem	mat2pmatval 22637*	The result of a matrix transformation. (Contributed by AV, 31-Jul-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑀𝑦))))
Theorem	mat2pmatvalel 22638	A (matrix) element of the result of a matrix transformation. (Contributed by AV, 31-Jul-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (𝑋(𝑇‘𝑀)𝑌) = (𝑆‘(𝑋𝑀𝑌)))
Theorem	mat2pmatbas 22639	The result of a matrix transformation is a polynomial matrix. (Contributed by AV, 1-Aug-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝐶))
Theorem	mat2pmatbas0 22640	The result of a matrix transformation is a polynomial matrix. (Contributed by AV, 27-Oct-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐻 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ 𝐻)
Theorem	mat2pmatf 22641	The matrix transformation is a function from the matrices to the polynomial matrices. (Contributed by AV, 27-Oct-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐻 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐵⟶𝐻)
Theorem	mat2pmatf1 22642	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.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐻 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐵–1-1→𝐻)
Theorem	mat2pmatghm 22643	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 22644*	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 22645	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 22646	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 22647	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 22648	The transformation of matrices into polynomial matrices is "linear", analogous to lmhmlin 20967. Since 𝐴 and 𝐶 have different scalar rings, 𝑇 cannot be a left module homomorphism as defined in df-lmhm 20954, see lmhmsca 20962. (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 22649	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 22650	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 22651	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 22652	The transformation of a matrix of dimenson 1. (Contributed by AV, 4-Aug-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅))    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = {⟨⟨𝐴, 𝐴⟩, (𝑆‘(𝐴𝑀𝐴))⟩})
Theorem	mat2pmatscmxcl 22653	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 22654	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 22655	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 22656	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 22657	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 22658	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 22659	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 22660	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 22661*	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 22662*	Value of the inverse matrix transformation. (Contributed by AV, 14-Dec-2019.)
⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅)    &   ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐼 = (𝑚 ∈ 𝑆 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
Theorem	cpm2mval 22663*	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 22664	A (matrix) element of the result of an inverse matrix transformation. (Contributed by AV, 14-Dec-2019.)
⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅)    &   ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (𝑋(𝐼‘𝑀)𝑌) = ((coe1‘(𝑋𝑀𝑌))‘0))
Theorem	cpm2mf 22665	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 22666	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 22667*	Lemma for m2cpminvid2 22668. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑛 ∈ ℕ0 ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))
Theorem	m2cpminvid2 22668	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 22669	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 22670	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 22671	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 22672	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 22673	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 22674	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 )
11.6.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 function decompPMat (see df-decpmat 22676), 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 22694.
Syntax	cdecpmat 22675	Extend class notation to include the decomposition of polynomial matrices.
class decompPMat
Definition	df-decpmat 22676*	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 22677*	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 22678*	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 22679	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 22680	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 22681*	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 22682*	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 22683	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 22684*	Lemma for decpmatmul 22685. (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 22685*	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 22686*	Lemma 0 for pm2mpmhm 22733. (Contributed by AV, 21-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 0 = (0g‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑙 ∈ ℕ0 ↦ (𝐴 Σg (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑙 − 𝑘)))))) finSupp 0 )
Theorem	pmatcollpw1lem1 22687*	Lemma 1 for pmatcollpw1 22689. (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 22688*	Lemma 2 for pmatcollpw1 22689: 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 22689*	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 22690*	Lemma for pmatcollpw2 22691. (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 22691*	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 22692	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 22683 (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 22693	Lemma for pmatcollpw 22694. (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 22694*	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 22695*	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 22696*	Lemma for pmatcollpw3 22697 and pmatcollpw3fi 22698: 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 22697*	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 22698*	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 22699*	Lemma 1 for pmatcollpw3fi1 22701. (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 22700*	Lemma 2 for pmatcollpw3fi1 22701. (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...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))))))