P. 228 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22701-22800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cpmatacl 22701*	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 22702*	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 22703*	Lemma for cpmatmcl 22704. (Contributed by AV, 18-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑐 ∈ ℕ ((coe1‘(𝑃 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑥𝑘)(.r‘𝑃)(𝑘𝑦𝑗)))))‘𝑐) = (0g‘𝑅))
Theorem	cpmatmcl 22704*	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 22705	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 22706	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 22707	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 22708*	Value of the matrix transformation. (Contributed by AV, 31-Jul-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦)))))
Theorem	mat2pmatval 22709*	The result of a matrix transformation. (Contributed by AV, 31-Jul-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑀𝑦))))
Theorem	mat2pmatvalel 22710	A (matrix) element of the result of a matrix transformation. (Contributed by AV, 31-Jul-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (𝑋(𝑇‘𝑀)𝑌) = (𝑆‘(𝑋𝑀𝑌)))
Theorem	mat2pmatbas 22711	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 22712	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 22713	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 22714	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 22715	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 22716*	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 22717	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 22718	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 22719	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 22720	The transformation of matrices into polynomial matrices is "linear", analogous to lmhmlin 20960. Since 𝐴 and 𝐶 have different scalar rings, 𝑇 cannot be a left module homomorphism as defined in df-lmhm 20947, see lmhmsca 20955. (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 22721	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 22722	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 22723	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 22724	The transformation of a matrix of dimenson 1. (Contributed by AV, 4-Aug-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅))    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = {⟨⟨𝐴, 𝐴⟩, (𝑆‘(𝐴𝑀𝐴))⟩})
Theorem	mat2pmatscmxcl 22725	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 22726	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 22727	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 22728	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 22729	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 22730	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 22731	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 22732	The transformed values of a (finite) mapping of integers to matrices. (Contributed by AV, 4-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑆 ∈ ℕ0) ∧ (𝑏 ∈ (𝐵 ↑m (0...𝑆)) ∧ 𝐼 ∈ (0...𝑆))) → (𝑇‘(𝑏‘𝐼)) ∈ (Base‘𝑌))
Theorem	m2pmfzgsumcl 22733*	Closure of the sum of scaled transformed matrices. (Contributed by AV, 4-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑌 = (𝑁 Mat 𝑃)    &   ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ · = ( ·𝑠 ‘𝑌)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖))))) ∈ (Base‘𝑌))
Theorem	cpm2mfval 22734*	Value of the inverse matrix transformation. (Contributed by AV, 14-Dec-2019.)
⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅)    &   ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐼 = (𝑚 ∈ 𝑆 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
Theorem	cpm2mval 22735*	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 22736	A (matrix) element of the result of an inverse matrix transformation. (Contributed by AV, 14-Dec-2019.)
⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅)    &   ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (𝑋(𝐼‘𝑀)𝑌) = ((coe1‘(𝑋𝑀𝑌))‘0))
Theorem	cpm2mf 22737	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 22738	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 22739*	Lemma for m2cpminvid2 22740. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑛 ∈ ℕ0 ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))
Theorem	m2cpminvid2 22740	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 22741	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 22742	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 22743	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 22744	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 22745	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 22746	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 22748), 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 22766.
Syntax	cdecpmat 22747	Extend class notation to include the decomposition of polynomial matrices.
class decompPMat
Definition	df-decpmat 22748*	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 22749*	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 22750*	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 22751	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 22752	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 22753*	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 22754*	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 22755	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 22756*	Lemma for decpmatmul 22757. (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 22757*	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 22758*	Lemma 0 for pm2mpmhm 22805. (Contributed by AV, 21-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 0 = (0g‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑙 ∈ ℕ0 ↦ (𝐴 Σg (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑙 − 𝑘)))))) finSupp 0 )
Theorem	pmatcollpw1lem1 22759*	Lemma 1 for pmatcollpw1 22761. (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 22760*	Lemma 2 for pmatcollpw1 22761: 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 22761*	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 22762*	Lemma for pmatcollpw2 22763. (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 22763*	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 22764	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 22755 (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 22765	Lemma for pmatcollpw 22766. (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 22766*	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 22767*	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 22768*	Lemma for pmatcollpw3 22769 and pmatcollpw3fi 22770: 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 22769*	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 22770*	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 22771*	Lemma 1 for pmatcollpw3fi1 22773. (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 22772*	Lemma 2 for pmatcollpw3fi1 22773. (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 22773*	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 22774	Lemma 1 for pmatcollpwscmat 22776. (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 22775	Lemma 2 for pmatcollpwscmat 22776. (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 22776*	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 22808, 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 22800 and pm2mprngiso 22807), and 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1 p ) 𝑘)𝑗) · (𝑘𝐸𝑌)))))) is the corresponding inverse function: (𝑇‘(𝐼‘𝑂)) = 𝑂) (see mp2pm2mp 22796). In this section, the following conventions are mostly used: 𝑅 is a (unital) ring (see df-ring 20213) 𝑃 = (Poly1‘𝑅) is the polynomial algebra over (the ring) 𝑅 (see df-ply1 22163) 𝐾 = (Base‘𝑃) is its base set (see df-base 17209) 𝑌 = (var1‘𝑅) is its variable (see df-vr1 22162) · = ( ·𝑠 ‘𝑃) is its scalar multiplication (see df-vsca 17278 or lmodvscl 20801) 𝐸 = (.g‘(mulGrp‘𝑃)) is its exponentiation (see df-mulg 19057) 𝐴 = (𝑁 Mat 𝑅) is the algebra of N x N matrices over (the ring) 𝑅 (see df-mat 22391) 𝐶 = (𝑁 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 22777	Extend class notation with the transformation of a polynomial matrix into a polynomial over matrices.
class pMatToMatPoly
Definition	df-pm2mp 22778*	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 22779*	Lemma for pm2mpf1 22784. (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 22780*	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 22781*	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 22782	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 22783	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 22784	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 22785	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 22786	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 22787*	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 22788*	Lemma for mply1topmatcl 22790. (Contributed by AV, 6-Oct-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝑘 ∈ ℕ0 ↦ ((𝐼((coe1‘𝑂)‘𝑘)𝐽) · (𝑘𝐸𝑌))) finSupp (0g‘𝑃))
Theorem	mply1topmatval 22789*	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 22796). (Contributed by AV, 6-Oct-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝐴)    &   ⊢ 𝐿 = (Base‘𝑄)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐸 = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑌 = (var1‘𝑅)    &   ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑂 ∈ 𝐿) → (𝐼‘𝑂) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))
Theorem	mply1topmatcl 22790*	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 22791*	Lemma 1 for mp2pm2mp 22796. (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 22792*	Lemma 2 for mp2pm2mp 22796. (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 22793*	Lemma 3 for mp2pm2mp 22796. (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 22794*	Lemma 4 for mp2pm2mp 22796. (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 22795*	Lemma 5 for mp2pm2mp 22796. (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 22796*	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 22797*	Lemma 2 for pm2mpghm 22801. (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 22798	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 22799	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 22800	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→𝐿)