P. 229 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22801-22900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	m2cpminv0 22801	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 22803), 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 22821.
Syntax	cdecpmat 22802	Extend class notation to include the decomposition of polynomial matrices.
class decompPMat
Definition	df-decpmat 22803*	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 22804*	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 22805*	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 22806	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 22807	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 22808*	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 22809*	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 22810	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 22811*	Lemma for decpmatmul 22812. (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 22812*	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 22813*	Lemma 0 for pm2mpmhm 22860. (Contributed by AV, 21-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 0 = (0g‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑙 ∈ ℕ0 ↦ (𝐴 Σg (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑙 − 𝑘)))))) finSupp 0 )
Theorem	pmatcollpw1lem1 22814*	Lemma 1 for pmatcollpw1 22816. (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 22815*	Lemma 2 for pmatcollpw1 22816: 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 22816*	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 22817*	Lemma for pmatcollpw2 22818. (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 22818*	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 22819	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 22810 (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 22820	Lemma for pmatcollpw 22821. (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 22821*	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 22822*	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 22823*	Lemma for pmatcollpw3 22824 and pmatcollpw3fi 22825: 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 22824*	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 22825*	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 22826*	Lemma 1 for pmatcollpw3fi1 22828. (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 22827*	Lemma 2 for pmatcollpw3fi1 22828. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝐶)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐷 = (Base‘𝐴)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑓 ∈ (𝐷 ↑m {0})𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) → ∃𝑠 ∈ ℕ ∃𝑓 ∈ (𝐷 ↑m (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))))))
Theorem	pmatcollpw3fi1 22828*	Write a polynomial matrix (over a commutative ring) as a finite sum of (at least two) products of variable powers and constant matrices with scalar entries. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝐶)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐷 = (Base‘𝐴)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑓 ∈ (𝐷 ↑m (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))
Theorem	pmatcollpwscmatlem1 22829	Lemma 1 for pmatcollpwscmat 22831. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝐶)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐷 = (Base‘𝐴)    &   ⊢ 𝑈 = (algSc‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐸 = (Base‘𝑃)    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ 1 = (1r‘𝐶)    &   ⊢ 𝑀 = (𝑄 ∗ 1 )    ⇒   ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (((coe1‘(𝑎𝑀𝑏))‘𝐿)( ·𝑠 ‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = if(𝑎 = 𝑏, (𝑈‘((coe1‘𝑄)‘𝐿)), (0g‘𝑃)))
Theorem	pmatcollpwscmatlem2 22830	Lemma 2 for pmatcollpwscmat 22831. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝐶)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐷 = (Base‘𝐴)    &   ⊢ 𝑈 = (algSc‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐸 = (Base‘𝑃)    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ 1 = (1r‘𝐶)    &   ⊢ 𝑀 = (𝑄 ∗ 1 )    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸)) → (𝑇‘(𝑀 decompPMat 𝐿)) = ((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 ))
Theorem	pmatcollpwscmat 22831*	Write a scalar matrix over polynomials (over a commutative ring) as a sum of the product of variable powers and constant scalar matrices with scalar entries. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝐶)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐷 = (Base‘𝐴)    &   ⊢ 𝑈 = (algSc‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐸 = (Base‘𝑃)    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ 1 = (1r‘𝐶)    &   ⊢ 𝑀 = (𝑄 ∗ 1 )    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸) → 𝑀 = (𝐶 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑋) ∗ ((𝑈‘((coe1‘𝑄)‘𝑛)) ∗ 1 )))))
11.6.4  Ring isomorphism between polynomial matrices and polynomials over matrices The main result of this section is Theorem pmmpric 22863, 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‘(𝑁 Mat 𝑅)) ≃ (𝑁 Mat (Poly1‘𝑅)) Or in a more common notation: (𝑁 Mat (Poly1‘𝑅)) corresponds to M(n, R[t]), the ring of n x n polynomial matrices over the ring R. (Poly1‘(𝑁 Mat 𝑅)) corresponds to M(n, R)[t], the polynomial ring over the ring of n x n matrices with entries in ring R. 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) with 𝐵 = (Base‘(𝑁 Mat (Poly1‘𝑅))) and (𝑚 decompPMat 𝑘) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1 ( i m j ) ) 𝑘))) is an isomorphism between these rings: 𝑇:𝐵–1-1-onto→𝐿 with 𝐿 = (Base‘(Poly1‘(𝑁 Mat 𝑅))) (see pm2mpf1o 22855 and pm2mprngiso 22862), and 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1 p ) 𝑘)𝑗) · (𝑘𝐸𝑌)))))) is the corresponding inverse function: (𝑇‘(𝐼‘𝑂)) = 𝑂) (see mp2pm2mp 22851). In this section, the following conventions are mostly used: 𝑅 is a (unital) ring (see df-ring 20264) 𝑃 = (Poly1‘𝑅) is the polynomial algebra over (the ring) 𝑅 (see df-ply1 22224) 𝐾 = (Base‘𝑃) is its base set (see df-base 17229) 𝑌 = (var1‘𝑅) is its variable (see df-vr1 22223) · = ( ·𝑠 ‘𝑃) is its scalar multiplication (see df-vsca 17286 or lmodvscl 20925) 𝐸 = (.g‘(mulGrp‘𝑃)) is its exponentiation (see df-mulg 19093) 𝐴 = (𝑁 Mat 𝑅) is the algebra of N x N matrices over (the ring) 𝑅 (see df-mat 22448) 𝐶 = (𝑁 Mat 𝑃) is the algebra of N x N matrices over (the polynomial ring) 𝑃. 𝐵 = (Base‘𝐶) is its base set 𝑀 ∈ 𝐵 is a concrete polynomial matrix 𝑄 = (Poly1‘𝐴) is the polynomial algebra over (the matrix ring) 𝐴. 𝐿 = (Base‘𝑄) is its base set 𝑂 ∈ 𝐿 is a concrete polynomial with matrix coefficients 𝑋 = (var1‘𝐴) is its variable ∗ = ( ·𝑠 ‘𝑄) is its scalar multiplication ↑ = (.g‘(mulGrp‘𝑄)) is its exponentiation
Syntax	cpm2mp 22832	Extend class notation with the transformation of a polynomial matrix into a polynomial over matrices.
class pMatToMatPoly
Definition	df-pm2mp 22833*	Transformation of a polynomial matrix (over a ring) into a polynomial over matrices (over the same ring). (Contributed by AV, 5-Dec-2019.)
⊢ pMatToMatPoly = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))))))
Theorem	pm2mpf1lem 22834*	Lemma for pm2mpf1 22839. (Contributed by AV, 14-Oct-2019.) (Revised by AV, 4-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0)) → ((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑈 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))))‘𝐾) = (𝑈 decompPMat 𝐾))
Theorem	pm2mpval 22835*	Value of the transformation of a polynomial matrix into a polynomial over matrices. (Contributed by AV, 5-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))))
Theorem	pm2mpfval 22836*	A polynomial matrix transformed into a polynomial over matrices. (Contributed by AV, 4-Oct-2019.) (Revised by AV, 5-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))))
Theorem	pm2mpcl 22837	The transformation of polynomial matrices into polynomials over matrices maps polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 5-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    &   ⊢ 𝐿 = (Base‘𝑄)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ 𝐿)
Theorem	pm2mpf 22838	The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 5-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    &   ⊢ 𝐿 = (Base‘𝑄)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐵⟶𝐿)
Theorem	pm2mpf1 22839	The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 14-Oct-2019.) (Revised by AV, 6-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    &   ⊢ 𝐿 = (Base‘𝑄)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐵–1-1→𝐿)
Theorem	pm2mpcoe1 22840	A coefficient of the polynomial over matrices which is the result of the transformation of a polynomial matrix is the matrix consisting of the coefficients in the polynomial entries of the polynomial matrix. (Contributed by AV, 20-Oct-2019.) (Revised by AV, 5-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0)) → ((coe1‘(𝑇‘𝑀))‘𝐾) = (𝑀 decompPMat 𝐾))
Theorem	idpm2idmp 22841	The transformation of the identity polynomial matrix into polynomials over matrices results in the identity of the polynomials over matrices. (Contributed by AV, 18-Oct-2019.) (Revised by AV, 5-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑇‘(1r‘𝐶)) = (1r‘𝑄))
Theorem	mptcoe1matfsupp 22842*	The mapping extracting the entries of the coefficient matrices of a polynomial over matrices at a fixed position is finitely supported. (Contributed by AV, 6-Oct-2019.) (Proof shortened by AV, 23-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝑘 ∈ ℕ0 ↦ (𝐼((coe1‘𝑂)‘𝑘)𝐽)) finSupp (0g‘𝑅))
Theorem	mply1topmatcllem 22843*	Lemma for mply1topmatcl 22845. (Contributed by AV, 6-Oct-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝑘 ∈ ℕ0 ↦ ((𝐼((coe1‘𝑂)‘𝑘)𝐽) · (𝑘𝐸𝑌))) finSupp (0g‘𝑃))
Theorem	mply1topmatval 22844*	A polynomial over matrices transformed into a polynomial matrix. 𝐼 is the inverse function of the transformation 𝑇 of polynomial matrices into polynomials over matrices: (𝑇‘(𝐼‘𝑂)) = 𝑂) (see mp2pm2mp 22851). (Contributed by AV, 6-Oct-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    &   ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑂 ∈ 𝐿) → (𝐼‘𝑂) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))
Theorem	mply1topmatcl 22845*	A polynomial over matrices transformed into a polynomial matrix is a polynomial matrix. (Contributed by AV, 6-Oct-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    &   ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝐼‘𝑂) ∈ 𝐵)
Theorem	mp2pm2mplem1 22846*	Lemma 1 for mp2pm2mp 22851. (Contributed by AV, 9-Oct-2019.) (Revised by AV, 5-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    &   ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝐼‘𝑂) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))
Theorem	mp2pm2mplem2 22847*	Lemma 2 for mp2pm2mp 22851. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 5-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    &   ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) ∈ 𝐵)
Theorem	mp2pm2mplem3 22848*	Lemma 3 for mp2pm2mp 22851. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 5-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    &   ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))    &   ⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)))
Theorem	mp2pm2mplem4 22849*	Lemma 4 for mp2pm2mp 22851. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    &   ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))    &   ⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝐾) = ((coe1‘𝑂)‘𝐾))
Theorem	mp2pm2mplem5 22850*	Lemma 5 for mp2pm2mp 22851. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    &   ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑘 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))) finSupp (0g‘𝑄))
Theorem	mp2pm2mp 22851*	A polynomial over matrices transformed into a polynomial matrix transformed back into the polynomial over matrices. (Contributed by AV, 12-Oct-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    &   ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑇‘(𝐼‘𝑂)) = 𝑂)
Theorem	pm2mpghmlem2 22852*	Lemma 2 for pm2mpghm 22856. (Contributed by AV, 15-Oct-2019.) (Revised by AV, 4-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))) finSupp (0g‘𝑄))
Theorem	pm2mpghmlem1 22853	Lemma 1 for pm2mpghm . (Contributed by AV, 15-Oct-2019.) (Revised by AV, 4-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ ℕ0) → ((𝑀 decompPMat 𝐾) ∗ (𝐾 ↑ 𝑋)) ∈ 𝐿)
Theorem	pm2mpfo 22854	The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 6-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐵–onto→𝐿)
Theorem	pm2mpf1o 22855	The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 14-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐵–1-1-onto→𝐿)
Theorem	pm2mpghm 22856	The transformation of polynomial matrices into polynomials over matrices is an additive group homomorphism. (Contributed by AV, 16-Oct-2019.) (Revised by AV, 6-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐶 GrpHom 𝑄))
Theorem	pm2mpgrpiso 22857	The transformation of polynomial matrices into polynomials over matrices is an additive group isomorphism. (Contributed by AV, 17-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐶 GrpIso 𝑄))
Theorem	pm2mpmhmlem1 22858*	Lemma 1 for pm2mpmhm 22860. (Contributed by AV, 21-Oct-2019.) (Revised by AV, 6-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑙 ∈ ℕ0 ↦ ((𝐴 Σg (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘)(.r‘𝐴)(𝑦 decompPMat (𝑙 − 𝑘))))) ∗ (𝑙 ↑ 𝑋))) finSupp (0g‘𝑄))
Theorem	pm2mpmhmlem2 22859*	Lemma 2 for pm2mpmhm 22860. (Contributed by AV, 22-Oct-2019.) (Revised by AV, 6-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦)))
Theorem	pm2mpmhm 22860	The transformation of polynomial matrices into polynomials over matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 22-Oct-2019.) (Revised by AV, 6-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ ((mulGrp‘𝐶) MndHom (mulGrp‘𝑄)))
Theorem	pm2mprhm 22861	The transformation of polynomial matrices into polynomials over matrices is a ring homomorphism. (Contributed by AV, 22-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐶 RingHom 𝑄))
Theorem	pm2mprngiso 22862	The transformation of polynomial matrices into polynomials over matrices is a ring isomorphism. (Contributed by AV, 22-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐶 RingIso 𝑄))
Theorem	pmmpric 22863	The ring of polynomial matrices over a ring is isomorphic to the ring of polynomials over matrices of the same dimension over the same ring. (Contributed by AV, 30-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ≃𝑟 𝑄)
Theorem	monmat2matmon 22864	The transformation of a polynomial matrix having scaled monomials with the same power as entries into a scaled monomial as a polynomial over matrices. (Contributed by AV, 11-Nov-2019.) (Revised by AV, 7-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐾 = (Base‘𝐴)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐼 = (𝑁 pMatToMatPoly 𝑅)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → (𝐼‘((𝐿𝐸𝑌) · (𝑇‘𝑀))) = (𝑀 ∗ (𝐿 ↑ 𝑋)))
Theorem	pm2mp 22865*	The transformation of a sum of matrices having scaled monomials with the same power as entries into a sum of scaled monomials as a polynomial over matrices. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 7-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ ∗ = ( ·𝑠 ‘𝑄)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑄))    &   ⊢ 𝑋 = (var1‘𝐴)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐾 = (Base‘𝐴)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐼 = (𝑁 pMatToMatPoly 𝑅)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑m ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → (𝐼‘(𝐶 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))))) = (𝑄 Σg (𝑛 ∈ ℕ0 ↦ ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋)))))
11.7  The characteristic polynomial According to Wikipedia ("Characteristic polynomial", 31-Jul-2019, https://en.wikipedia.org/wiki/Characteristic_polynomial): "In linear algebra, the characteristic polynomial of a square matrix is a polynomial which is invariant under matrix similarity and has the eigenvalues as roots. It has the determinant and the trace of the matrix as coefficients.". Based on the definition of the characteristic polynomial of a square matrix (df-chpmat 22867) the eigenvalues and corresponding eigenvectors can be defined.
11.7.1  Definition and basic properties The characteristic polynomial of a matrix 𝐴 is the determinant of the characteristic matrix of 𝐴: (𝑡𝐼 − 𝐴).
Syntax	cchpmat 22866	Extend class notation with the characteristic polynomial.
class CharPlyMat
Definition	df-chpmat 22867*	Define the characteristic polynomial of a square matrix. According to Wikipedia ("Characteristic polynomial", 31-Jul-2019, https://en.wikipedia.org/wiki/Characteristic_polynomial): "The characteristic polynomial of [an n x n matrix] A, denoted by pA(t), is the polynomial defined by pA ( t ) = det ( t I - A ) where I denotes the n-by-n identity matrix.". In addition, however, the underlying ring must be commutative, see definition in [Lang], p. 561: " Let k be a commutative ring ... Let M be any n x n matrix in k ... We define the characteristic polynomial PM(t) to be the determinant det ( t In - M ) where In is the unit n x n matrix." To be more precise, the matrices A and I on the right hand side are matrices with coefficients of a polynomial ring. Therefore, the original matrix A over a given commutative ring must be transformed into corresponding matrices over the polynomial ring over the given ring. (Contributed by AV, 2-Aug-2019.)
⊢ CharPlyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ ((𝑛 maDet (Poly1‘𝑟))‘(((var1‘𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1‘𝑟)))(1r‘(𝑛 Mat (Poly1‘𝑟))))(-g‘(𝑛 Mat (Poly1‘𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚)))))
Theorem	chmatcl 22868	Closure of the characteristic matrix of a matrix. (Contributed by AV, 25-Oct-2019.) (Proof shortened by AV, 29-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ − = (-g‘𝑌)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ 𝐻 = ((𝑋 · 1 ) − (𝑇‘𝑀))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝐻 ∈ (Base‘𝑌))
Theorem	chmatval 22869	The entries of the characteristic matrix of a matrix. (Contributed by AV, 2-Aug-2019.) (Proof shortened by AV, 10-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ − = (-g‘𝑌)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ 𝐻 = ((𝑋 · 1 ) − (𝑇‘𝑀))    &   ⊢ ∼ = (-g‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼𝐻𝐽) = if(𝐼 = 𝐽, (𝑋 ∼ (𝐼(𝑇‘𝑀)𝐽)), ( 0 ∼ (𝐼(𝑇‘𝑀)𝐽))))
Theorem	chpmatfval 22870*	Value of the characteristic polynomial function. (Contributed by AV, 2-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝐷 = (𝑁 maDet 𝑃)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 1 = (1r‘𝑌)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐶 = (𝑚 ∈ 𝐵 ↦ (𝐷‘((𝑋 · 1 ) − (𝑇‘𝑚)))))
Theorem	chpmatval 22871	The characteristic polynomial of a (square) matrix (expressed with a determinant). (Contributed by AV, 2-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝐷 = (𝑁 maDet 𝑃)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 1 = (1r‘𝑌)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) = (𝐷‘((𝑋 · 1 ) − (𝑇‘𝑀))))
Theorem	chpmatply1 22872	The characteristic polynomial of a (square) matrix over a commutative ring is a polynomial, see also the following remark in [Lang], p. 561: "[the characteristic polynomial] is an element of k[t]". (Contributed by AV, 2-Aug-2019.) (Proof shortened by AV, 29-Nov-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐸 = (Base‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) ∈ 𝐸)
Theorem	chpmatval2 22873*	The characteristic polynomial of a (square) matrix (expressed with the Leibnitz formula for the determinant). (Contributed by AV, 2-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ 𝐺 = (SymGrp‘𝑁)    &   ⊢ 𝐻 = (Base‘𝐺)    &   ⊢ 𝑍 = (ℤRHom‘𝑃)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 𝑈 = (mulGrp‘𝑃)    &   ⊢ × = (.r‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) = (𝑃 Σg (𝑝 ∈ 𝐻 ↦ (((𝑍 ∘ 𝑆)‘𝑝) × (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)((𝑋 · 1 ) − (𝑇‘𝑀))𝑥)))))))
Theorem	chpmat0d 22874	The characteristic polynomial of the empty matrix. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐶 = (∅ CharPlyMat 𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐶‘∅) = (1r‘(Poly1‘𝑅)))
Theorem	chpmat1dlem 22875	Lemma for chpmat1d 22876. (Contributed by AV, 7-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ 𝐺 = (𝑁 Mat 𝑃)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼((𝑋( ·𝑠 ‘𝐺)(1r‘𝐺))(-g‘𝐺)(𝑇‘𝑀))𝐼) = (𝑋 − (𝑆‘(𝐼𝑀𝐼))))
Theorem	chpmat1d 22876	The characteristic polynomial of a matrix with dimension 1. (Contributed by AV, 7-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) = (𝑋 − (𝑆‘(𝐼𝑀𝐼))))
Theorem	chpdmatlem0 22877	Lemma 0 for chpdmat 22881. (Contributed by AV, 18-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝑄 = (𝑁 Mat 𝑃)    &   ⊢ 1 = (1r‘𝑄)    &   ⊢ · = ( ·𝑠 ‘𝑄)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋 · 1 ) ∈ (Base‘𝑄))
Theorem	chpdmatlem1 22878	Lemma 1 for chpdmat 22881. (Contributed by AV, 18-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝑄 = (𝑁 Mat 𝑃)    &   ⊢ 1 = (1r‘𝑄)    &   ⊢ · = ( ·𝑠 ‘𝑄)    &   ⊢ 𝑍 = (-g‘𝑄)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑋 · 1 )𝑍(𝑇‘𝑀)) ∈ (Base‘𝑄))
Theorem	chpdmatlem2 22879	Lemma 2 for chpdmat 22881. (Contributed by AV, 18-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝑄 = (𝑁 Mat 𝑃)    &   ⊢ 1 = (1r‘𝑄)    &   ⊢ · = ( ·𝑠 ‘𝑄)    &   ⊢ 𝑍 = (-g‘𝑄)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    ⇒   ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ 𝑖 ≠ 𝑗) ∧ (𝑖𝑀𝑗) = 0 ) → (𝑖((𝑋 · 1 )𝑍(𝑇‘𝑀))𝑗) = (0g‘𝑃))
Theorem	chpdmatlem3 22880	Lemma 3 for chpdmat 22881. (Contributed by AV, 18-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝑄 = (𝑁 Mat 𝑃)    &   ⊢ 1 = (1r‘𝑄)    &   ⊢ · = ( ·𝑠 ‘𝑄)    &   ⊢ 𝑍 = (-g‘𝑄)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → (𝐾((𝑋 · 1 )𝑍(𝑇‘𝑀))𝐾) = (𝑋 − (𝑆‘(𝐾𝑀𝐾))))
Theorem	chpdmat 22881*	The characteristic polynomial of a diagonal matrix. (Contributed by AV, 18-Aug-2019.) (Proof shortened by AV, 21-Nov-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ − = (-g‘𝑃)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) → (𝐶‘𝑀) = (𝐺 Σg (𝑘 ∈ 𝑁 ↦ (𝑋 − (𝑆‘(𝑘𝑀𝑘))))))
Theorem	chpscmat 22882*	The characteristic polynomial of a (nonempty!) scalar matrix. (Contributed by AV, 21-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝐷 = {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))}    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ − = (-g‘𝑃)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → (𝐶‘𝑀) = ((♯‘𝑁) ↑ (𝑋 − (𝑆‘𝐸))))
Theorem	chpscmat0 22883*	The characteristic polynomial of a (nonempty!) scalar matrix, expressed with its diagonal element. (Contributed by AV, 21-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝐷 = {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))}    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ − = (-g‘𝑃)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐼𝑀𝐼))) → (𝐶‘𝑀) = ((♯‘𝑁) ↑ (𝑋 − (𝑆‘(𝐼𝑀𝐼)))))
Theorem	chpscmatgsumbin 22884*	The characteristic polynomial of a (nonempty!) scalar matrix, expressed as finite group sum of binomials. (Contributed by AV, 2-Sep-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝐷 = {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))}    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐹 = (.g‘𝑃)    &   ⊢ 𝐻 = (mulGrp‘𝑅)    &   ⊢ 𝐸 = (.g‘𝐻)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) → (𝐶‘𝑀) = (𝑃 Σg (𝑙 ∈ (0...(♯‘𝑁)) ↦ (((♯‘𝑁)C𝑙)𝐹((((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽))) · (𝑙 ↑ 𝑋))))))
Theorem	chpscmatgsummon 22885*	The characteristic polynomial of a (nonempty!) scalar matrix, expressed as finite group sum of scaled monomials. (Contributed by AV, 2-Sep-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝐷 = {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))}    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐹 = (.g‘𝑃)    &   ⊢ 𝐻 = (mulGrp‘𝑅)    &   ⊢ 𝐸 = (.g‘𝐻)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝑍 = (.g‘𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) → (𝐶‘𝑀) = (𝑃 Σg (𝑙 ∈ (0...(♯‘𝑁)) ↦ ((((♯‘𝑁)C𝑙)𝑍(((♯‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽)))) · (𝑙 ↑ 𝑋)))))
Theorem	chp0mat 22886	The characteristic polynomial of the zero matrix. (Contributed by AV, 18-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐴)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐶‘ 0 ) = ((♯‘𝑁) ↑ 𝑋))
Theorem	chpidmat 22887	The characteristic polynomial of the identity matrix. (Contributed by AV, 19-Aug-2019.)
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝐼 = (1r‘𝐴)    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ − = (-g‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐶‘𝐼) = ((♯‘𝑁) ↑ (𝑋 − (𝑆‘ 1 ))))
Theorem	chmaidscmat 22888	The characteristic polynomial of a matrix multiplied with the identity matrix is a scalar matrix. (Contributed by AV, 30-Oct-2019.) (Revised by AV, 5-Jul-2022.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐸 = (Base‘𝑃)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝐾 = (Base‘𝑌)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝐶‘𝑀) · 1 ) ∈ 𝑆)
11.7.2  The characteristic factor function G In this subsection the function 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) is discussed. This function is involved in the representation of the product of the characteristic matrix of a given matrix and its adjunct as an infinite sum, see cpmadugsum 22918. Therefore, this function is called "characteristic factor function" (in short "chfacf") in the following. It plays an important role in the proof of the Cayley-Hamilton theorem, see cayhamlem1 22906, cayhamlem3 22927 and cayhamlem4 22928.
Theorem	fvmptnn04if 22889*	The function values of a mapping from the nonnegative integers with four distinct cases. (Contributed by AV, 10-Nov-2019.)
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))))    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑁 = 0) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐴)    &   ⊢ ((𝜑 ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐵)    &   ⊢ ((𝜑 ∧ 𝑁 = 𝑆) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐶)    &   ⊢ ((𝜑 ∧ 𝑆 < 𝑁) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐷)    ⇒   ⊢ (𝜑 → (𝐺‘𝑁) = 𝑌)
Theorem	fvmptnn04ifa 22890*	The function value of a mapping from the nonnegative integers with four distinct cases for the first case. (Contributed by AV, 10-Nov-2019.)
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))))    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ ((𝜑 ∧ 𝑁 = 0 ∧ ⦋𝑁 / 𝑛⦌𝐴 ∈ 𝑉) → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌𝐴)
Theorem	fvmptnn04ifb 22891*	The function value of a mapping from the nonnegative integers with four distinct cases for the second case. (Contributed by AV, 10-Nov-2019.)
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))))    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌𝐵)
Theorem	fvmptnn04ifc 22892*	The function value of a mapping from the nonnegative integers with four distinct cases for the third case. (Contributed by AV, 10-Nov-2019.)
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))))    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ ((𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋𝑁 / 𝑛⦌𝐶 ∈ 𝑉) → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌𝐶)
Theorem	fvmptnn04ifd 22893*	The function value of a mapping from the nonnegative integers with four distinct cases for the forth case. (Contributed by AV, 10-Nov-2019.)
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))))    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ ((𝜑 ∧ 𝑆 < 𝑁 ∧ ⦋𝑁 / 𝑛⦌𝐷 ∈ 𝑉) → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌𝐷)
Theorem	chfacfisf 22894*	The "characteristic factor function" is a function from the nonnegative integers to polynomial matrices. (Contributed by AV, 8-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌))
Theorem	chfacfisfcpmat 22895*	The "characteristic factor function" is a function from the nonnegative integers to constant polynomial matrices. (Contributed by AV, 19-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶𝑆)
Theorem	chfacffsupp 22896*	The "characteristic factor function" is finitely supported. (Contributed by AV, 20-Nov-2019.) (Proof shortened by AV, 23-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺 finSupp (0g‘𝑌))
Theorem	chfacfscmulcl 22897*	Closure of a scaled value of the "characteristic factor function". (Contributed by AV, 9-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝐾 ∈ ℕ0) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) ∈ (Base‘𝑌))
Theorem	chfacfscmul0 22898*	A scaled value of the "characteristic factor function" is zero almost always. (Contributed by AV, 9-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝐾 ∈ (ℤ≥‘(𝑠 + 2))) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = 0 )
Theorem	chfacfscmulfsupp 22899*	A mapping of scaled values of the "characteristic factor function" is finitely supported. (Contributed by AV, 8-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))) finSupp 0 )
Theorem	chfacfscmulgsum 22900*	Breaking up a sum of values of the "characteristic factor function" scaled by a polynomial. (Contributed by AV, 9-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ × = (.r‘𝑌)    &   ⊢ − = (-g‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ + = (+g‘𝑌)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))))