P. 210 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20901-21000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cramerlem2 20901*	Lemma 2 for cramer 20904. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ∀𝑧 ∈ 𝑉 ((𝑋 · 𝑧) = 𝑌 → 𝑧 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋)))))
Theorem	cramerlem3 20902*	Lemma 3 for cramer 20904. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌))
Theorem	cramer0 20903*	Special case of Cramer's rule for 0-dimensional matrices/vectors. (Contributed by AV, 28-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌))
Theorem	cramer 20904*	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 20899). 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 20890 or slesolinv 20892. 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‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ (𝑋 · 𝑍) = 𝑌))
11.4  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.4.1  Basic properties
Theorem	pmatring 20905	The set of polynomial matrices over a ring is a ring. (Contributed by AV, 6-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring)
Theorem	pmatlmod 20906	The set of polynomial matrices over a ring is a left module. (Contributed by AV, 6-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ LMod)
Theorem	pmat0op 20907*	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 20908*	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 20909	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 20910*	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/algebraic scalars function algSc). (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝐴‘ 0 )))
Theorem	pmat1opsc 20911*	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 20912	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 20913*	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 20914	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.4.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 19711) to a scalar 𝐴 ∈ 𝑅: ((algSc‘𝑃)‘𝐴). In an analogous way, constant polynomial matrices (over the ring 𝑅) are obtained by "lifting" matrices over the ring 𝑅 by the function matToPolyMat (see df-mat2pmat 20919), 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 20933) and that 𝑇 = (𝑁 matToPolyMat 𝑅) is a ring isomorphism between the ring of matrices over a ring 𝑅 and the ring of constant polynomial matrices over the ring 𝑅 (see m2cpmrngiso 20970). By this, it is shown that the ring of matrices over a commutative ring is isomorphic to the ring of scalar matrices over the same ring, see matcpmric 20971. Finally 𝐼 = (𝑁 cPolyMatToMat 𝑅), the transformation of a constant polynomial matrix into a matrix, is the inverse function of the matrix transformation 𝑇 = (𝑁 matToPolyMat 𝑅), see m2cpminv 20972.
Syntax	ccpmat 20915	Extend class notation with the set of all constant polynomial matrices.
class ConstPolyMat
Syntax	cmat2pmat 20916	Extend class notation with the transformation of a matrix into a matrix of polynomials.
class matToPolyMat
Syntax	ccpmat2mat 20917	Extend class notation with the transformation of a constant polynomial matrix into a matrix.
class cPolyMatToMat
Definition	df-cpmat 20918*	The set of all constant polynomial matrices, which are all matrices whose entries are constant polynomials (or "scalar polynomials", see ply1sclf 20051). (Contributed by AV, 15-Nov-2019.)
⊢ ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)})
Definition	df-mat2pmat 20919*	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 20920*	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 20972, it is also called "inverse matrix transformation" in the following. (Contributed by AV, 14-Dec-2019.)
⊢ cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
Theorem	cpmat 20921*	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 20922	A constant polynomial matrix is a polynomial matrix. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) → 𝑀 ∈ 𝐵)
Theorem	cpmatel 20923*	Property of a constant polynomial matrix. (Contributed by AV, 15-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑀 ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅)))
Theorem	cpmatelimp 20924*	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 20925*	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 20926*	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 20927	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 20928*	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 20929*	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 20930*	Lemma for cpmatmcl 20931. (Contributed by AV, 18-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑐 ∈ ℕ ((coe1‘(𝑃 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑥𝑘)(.r‘𝑃)(𝑘𝑦𝑗)))))‘𝑐) = (0g‘𝑅))
Theorem	cpmatmcl 20931*	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 20932	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 20933	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 20934	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 20935*	Value of the matrix transformation. (Contributed by AV, 31-Jul-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦)))))
Theorem	mat2pmatval 20936*	The result of a matrix transformation. (Contributed by AV, 31-Jul-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑀𝑦))))
Theorem	mat2pmatvalel 20937	A (matrix) element of the result of a matrix transformation. (Contributed by AV, 31-Jul-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (𝑋(𝑇‘𝑀)𝑌) = (𝑆‘(𝑋𝑀𝑌)))
Theorem	mat2pmatbas 20938	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 20939	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 20940	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 20941	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 20942	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 20943*	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 20944	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 20945	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 20946	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 20947	The transformation of matrices into polynomial matrices is "linear", analogous to lmhmlin 19430. Since 𝐴 and 𝐶 have different scalar rings, 𝑇 cannot be a left module homomorphism as defined in df-lmhm 19417, see lmhmsca 19425. (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 20948	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 20949	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 20950	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 20951	The transformation of a matrix of dimenson 1. (Contributed by AV, 4-Aug-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅))    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = {⟨⟨𝐴, 𝐴⟩, (𝑆‘(𝐴𝑀𝐴))⟩})
Theorem	mat2pmatscmxcl 20952	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 20953	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 20954	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 20955	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 20956	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 20957	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 20958	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 20959	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) ∧ (𝑏 ∈ (𝐵 ↑𝑚 (0...𝑆)) ∧ 𝐼 ∈ (0...𝑆))) → (𝑇‘(𝑏‘𝐼)) ∈ (Base‘𝑌))
Theorem	m2pmfzgsumcl 20960*	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 ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖))))) ∈ (Base‘𝑌))
Theorem	cpm2mfval 20961*	Value of the inverse matrix transformation. (Contributed by AV, 14-Dec-2019.)
⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅)    &   ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐼 = (𝑚 ∈ 𝑆 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
Theorem	cpm2mval 20962*	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 20963	A (matrix) element of the result of an inverse matrix transformation. (Contributed by AV, 14-Dec-2019.)
⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅)    &   ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (𝑋(𝐼‘𝑀)𝑌) = ((coe1‘(𝑋𝑀𝑌))‘0))
Theorem	cpm2mf 20964	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 20965	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 20966*	Lemma for m2cpminvid2 20967. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑛 ∈ ℕ0 ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))
Theorem	m2cpminvid2 20967	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 20968	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 20969	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 20970	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 20971	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 20972	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 20973	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.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 20975), 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 20993.
Syntax	cdecpmat 20974	Extend class notation to include the decomposition of polynomial matrices.
class decompPMat
Definition	df-decpmat 20975*	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 20976*	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 20977*	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 20978	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 20979	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 20980*	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 20981*	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 20982	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 20983*	Lemma for decpmatmul 20984. (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 20984*	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 20985*	Lemma 0 for pm2mpmhm 21032. (Contributed by AV, 21-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 0 = (0g‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑙 ∈ ℕ0 ↦ (𝐴 Σg (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑙 − 𝑘)))))) finSupp 0 )
Theorem	pmatcollpw1lem1 20986*	Lemma 1 for pmatcollpw1 20988. (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 20987*	Lemma 2 for pmatcollpw1 20988: 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 20988*	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 20989*	Lemma for pmatcollpw2 20990. (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 20990*	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 20991	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 20982 (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 20992	Lemma for pmatcollpw 20993. (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 20993*	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 20994*	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 20995*	Lemma for pmatcollpw3 20996 and pmatcollpw3fi 20997: 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 𝑛))))) → ∃𝑓 ∈ (𝐷 ↑𝑚 𝐼)𝑀 = (𝐶 Σg (𝑛 ∈ 𝐼 ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))))))
Theorem	pmatcollpw3 20996*	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 ∧ 𝑀 ∈ 𝐵) → ∃𝑓 ∈ (𝐷 ↑𝑚 ℕ0)𝑀 = (𝐶 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))
Theorem	pmatcollpw3fi 20997*	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 ∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))
Theorem	pmatcollpw3fi1lem1 20998*	Lemma 1 for pmatcollpw3fi1 21000. (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) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛))))))
Theorem	pmatcollpw3fi1lem2 20999*	Lemma 2 for pmatcollpw3fi1 21000. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝐶)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐷 = (Base‘𝐴)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑓 ∈ (𝐷 ↑𝑚 {0})𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) → ∃𝑠 ∈ ℕ ∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))))))
Theorem	pmatcollpw3fi1 21000*	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 ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))