| Metamath
Proof Explorer Theorem List (p. 228 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | pmat0op 22701* | The zero polynomial matrix over a ring represented as operation. (Contributed by AV, 16-Nov-2019.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 0 )) | ||
| Theorem | pmat1op 22702* | The identity polynomial matrix over a ring represented as operation. (Contributed by AV, 16-Nov-2019.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ 1 = (1r‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, 1 , 0 ))) | ||
| Theorem | pmat1ovd 22703 | Entries of the identity polynomial matrix over a ring, deduction form. (Contributed by AV, 16-Nov-2019.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ 1 = (1r‘𝑃) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) & ⊢ (𝜑 → 𝐽 ∈ 𝑁) & ⊢ 𝑈 = (1r‘𝐶) ⇒ ⊢ (𝜑 → (𝐼𝑈𝐽) = if(𝐼 = 𝐽, 1 , 0 )) | ||
| Theorem | pmat0opsc 22704* | The zero polynomial matrix over a ring represented as operation with "lifted scalars" (i.e. elements of the ring underlying the polynomial ring embedded into the polynomial ring by the scalar injection/algebra scalar lifting function algSc). (Contributed by AV, 16-Nov-2019.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝐴‘ 0 ))) | ||
| Theorem | pmat1opsc 22705* | The identity polynomial matrix over a ring represented as operation with "lifted scalars". (Contributed by AV, 16-Nov-2019.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝐴‘ 1 ), (𝐴‘ 0 )))) | ||
| Theorem | pmat1ovscd 22706 | Entries of the identity polynomial matrix over a ring represented with "lifted scalars", deduction form. (Contributed by AV, 16-Nov-2019.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) & ⊢ (𝜑 → 𝐽 ∈ 𝑁) & ⊢ 𝑈 = (1r‘𝐶) ⇒ ⊢ (𝜑 → (𝐼𝑈𝐽) = if(𝐼 = 𝐽, (𝐴‘ 1 ), (𝐴‘ 0 ))) | ||
| Theorem | pmatcoe1fsupp 22707* | For a polynomial matrix there is an upper bound for the coefficients of all the polynomials being not 0. (Contributed by AV, 3-Oct-2019.) (Proof shortened by AV, 28-Nov-2019.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 )) | ||
| Theorem | 1pmatscmul 22708 | The scalar product of the identity polynomial matrix with a polynomial is a polynomial matrix. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐸 = (Base‘𝑃) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ 1 = (1r‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸) → (𝑄 ∗ 1 ) ∈ 𝐵) | ||
A constant polynomial matrix is a polynomial matrix whose elements are constant polynomials, i.e., polynomials with no indeterminates. Constant polynomials are obtained by "lifting" a "scalar" (i.e. an element of the underlying ring) into the polynomial ring/algebra by a "scalar injection", i.e., applying the "algebra scalar injection function" algSc (see df-ascl 21875) to a scalar 𝐴 ∈ 𝑅: ((algSc‘𝑃)‘𝐴). Analogously, constant polynomial matrices (over the ring 𝑅) are obtained by "lifting" matrices over the ring 𝑅 by the function matToPolyMat (see df-mat2pmat 22713), called "matrix transformation" in the following. In this section it is shown that the set 𝑆 = (𝑁 ConstPolyMat 𝑅) of constant polynomial 𝑁 x 𝑁 matrices over the ring 𝑅 is a subring of the ring of polynomial 𝑁 x 𝑁 matrices over the ring 𝑅 (cpmatsrgpmat 22727) and that 𝑇 = (𝑁 matToPolyMat 𝑅) is a ring isomorphism from the ring of matrices over a ring 𝑅 onto the ring of constant polynomial matrices over the ring 𝑅 (see m2cpmrngiso 22764). Thus, the ring of matrices over a commutative ring is isomorphic to the ring of scalar matrices over the same ring, see matcpmric 22765. Finally, 𝐼 = (𝑁 cPolyMatToMat 𝑅), the transformation of a constant polynomial matrix into a matrix, is the inverse function of the matrix transformation 𝑇 = (𝑁 matToPolyMat 𝑅), see m2cpminv 22766. | ||
| Syntax | ccpmat 22709 | Extend class notation with the set of all constant polynomial matrices. |
| class ConstPolyMat | ||
| Syntax | cmat2pmat 22710 | Extend class notation with the transformation of a matrix into a matrix of polynomials. |
| class matToPolyMat | ||
| Syntax | ccpmat2mat 22711 | Extend class notation with the transformation of a constant polynomial matrix into a matrix. |
| class cPolyMatToMat | ||
| Definition | df-cpmat 22712* | The set of all constant polynomial matrices, which are all matrices whose entries are constant polynomials (or "scalar polynomials", see ply1sclf 22288). (Contributed by AV, 15-Nov-2019.) |
| ⊢ ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)}) | ||
| Definition | df-mat2pmat 22713* | Transformation of a matrix (over a ring) into a matrix over the corresponding polynomial ring. (Contributed by AV, 31-Jul-2019.) |
| ⊢ matToPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦))))) | ||
| Definition | df-cpmat2mat 22714* | Transformation of a constant polynomial matrix (over a ring) into a matrix over the corresponding ring. Since this function is the inverse function of matToPolyMat, see m2cpminv 22766, it is also called "inverse matrix transformation" in the following. (Contributed by AV, 14-Dec-2019.) |
| ⊢ cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))) | ||
| Theorem | cpmat 22715* | Value of the constructor of the set of all constant polynomial matrices, i.e. the set of all 𝑁 x 𝑁 matrices of polynomials over a ring 𝑅. (Contributed by AV, 15-Nov-2019.) |
| ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑆 = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)}) | ||
| Theorem | cpmatpmat 22716 | A constant polynomial matrix is a polynomial matrix. (Contributed by AV, 16-Nov-2019.) |
| ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) → 𝑀 ∈ 𝐵) | ||
| Theorem | cpmatel 22717* | Property of a constant polynomial matrix. (Contributed by AV, 15-Nov-2019.) |
| ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑀 ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅))) | ||
| Theorem | cpmatelimp 22718* | Implication of a set being a constant polynomial matrix. (Contributed by AV, 18-Nov-2019.) |
| ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝑆 → (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅)))) | ||
| Theorem | cpmatel2 22719* | Another property of a constant polynomial matrix. (Contributed by AV, 16-Nov-2019.) (Proof shortened by AV, 27-Nov-2019.) |
| ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑀 ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑘 ∈ 𝐾 (𝑖𝑀𝑗) = (𝐴‘𝑘))) | ||
| Theorem | cpmatelimp2 22720* | Another implication of a set being a constant polynomial matrix. (Contributed by AV, 17-Nov-2019.) |
| ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝑆 → (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑘 ∈ 𝐾 (𝑖𝑀𝑗) = (𝐴‘𝑘)))) | ||
| Theorem | 1elcpmat 22721 | The identity of the ring of all polynomial matrices over the ring 𝑅 is a constant polynomial matrix. (Contributed by AV, 16-Nov-2019.) |
| ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r‘𝐶) ∈ 𝑆) | ||
| Theorem | cpmatacl 22722* | 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 22723* | 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 22724* | Lemma for cpmatmcl 22725. (Contributed by AV, 18-Nov-2019.) |
| ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑐 ∈ ℕ ((coe1‘(𝑃 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑥𝑘)(.r‘𝑃)(𝑘𝑦𝑗)))))‘𝑐) = (0g‘𝑅)) | ||
| Theorem | cpmatmcl 22725* | 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 22726 | 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 22727 | 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 22728 | 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 22729* | Value of the matrix transformation. (Contributed by AV, 31-Jul-2019.) |
| ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦))))) | ||
| Theorem | mat2pmatval 22730* | The result of a matrix transformation. (Contributed by AV, 31-Jul-2019.) |
| ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑀𝑦)))) | ||
| Theorem | mat2pmatvalel 22731 | A (matrix) element of the result of a matrix transformation. (Contributed by AV, 31-Jul-2019.) |
| ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (𝑋(𝑇‘𝑀)𝑌) = (𝑆‘(𝑋𝑀𝑌))) | ||
| Theorem | mat2pmatbas 22732 | 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 22733 | 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 22734 | 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 22735 | 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 22736 | 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 22737* | 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 22738 | 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 22739 | 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 22740 | 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 22741 | The transformation of matrices into polynomial matrices is "linear", analogous to lmhmlin 21034. Since 𝐴 and 𝐶 have different scalar rings, 𝑇 cannot be a left module homomorphism as defined in df-lmhm 21021, see lmhmsca 21029. (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 22742 | 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 22743 | 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 22744 | 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 22745 | The transformation of a matrix of dimenson 1. (Contributed by AV, 4-Aug-2019.) |
| ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉}) | ||
| Theorem | mat2pmatscmxcl 22746 | 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 22747 | 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 22748 | 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 22749 | 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 22750 | 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 22751 | 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 22752 | 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 22753 | 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 22754* | 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 22755* | Value of the inverse matrix transformation. (Contributed by AV, 14-Dec-2019.) |
| ⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅) & ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐼 = (𝑚 ∈ 𝑆 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))) | ||
| Theorem | cpm2mval 22756* | 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 22757 | A (matrix) element of the result of an inverse matrix transformation. (Contributed by AV, 14-Dec-2019.) |
| ⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅) & ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (𝑋(𝐼‘𝑀)𝑌) = ((coe1‘(𝑋𝑀𝑌))‘0)) | ||
| Theorem | cpm2mf 22758 | 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 22759 | 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 22760* | Lemma for m2cpminvid2 22761. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.) |
| ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑛 ∈ ℕ0 ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) | ||
| Theorem | m2cpminvid2 22761 | 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 22762 | 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 22763 | 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 22764 | 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 22765 | 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 22766 | 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 22767 | 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 ) | ||
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 22769), 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 22787. | ||
| Syntax | cdecpmat 22768 | Extend class notation to include the decomposition of polynomial matrices. |
| class decompPMat | ||
| Definition | df-decpmat 22769* | 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 22770* | 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 22771* | 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 22772 | 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 22773 | 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 22774* | 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 22775* | 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 22776 | 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 22777* | Lemma for decpmatmul 22778. (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 22778* | 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 22779* | Lemma 0 for pm2mpmhm 22826. (Contributed by AV, 21-Oct-2019.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ · = (.r‘𝐴) & ⊢ 0 = (0g‘𝐴) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑙 ∈ ℕ0 ↦ (𝐴 Σg (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑙 − 𝑘)))))) finSupp 0 ) | ||
| Theorem | pmatcollpw1lem1 22780* | Lemma 1 for pmatcollpw1 22782. (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 22781* | Lemma 2 for pmatcollpw1 22782: 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 22782* | 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 22783* | Lemma for pmatcollpw2 22784. (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 22784* | 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 22785 | 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 22776 (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 22786 | Lemma for pmatcollpw 22787. (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 22787* | 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 22788* | 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 22789* | Lemma for pmatcollpw3 22790 and pmatcollpw3fi 22791: 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 22790* | 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 22791* | 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 22792* | Lemma 1 for pmatcollpw3fi1 22794. (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 22793* | Lemma 2 for pmatcollpw3fi1 22794. (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 22794* | 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 22795 | Lemma 1 for pmatcollpwscmat 22797. (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 22796 | Lemma 2 for pmatcollpwscmat 22797. (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 22797* | 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 ))))) | ||
The main result of this section is Theorem pmmpric 22829, 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:
| ||
| Syntax | cpm2mp 22798 | Extend class notation with the transformation of a polynomial matrix into a polynomial over matrices. |
| class pMatToMatPoly | ||
| Definition | df-pm2mp 22799* | 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 22800* | Lemma for pm2mpf1 22805. (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 𝐾)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |