![]() |
Metamath
Proof Explorer Theorem List (p. 228 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | slesolinv 22701 | The solution of a system of linear equations represented by a matrix with a unit as determinant is the multiplication of the inverse of the matrix with the right-hand side vector. (Contributed by AV, 10-Feb-2019.) (Revised by AV, 28-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐼 = (invr‘𝐴) ⇒ ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝐷‘𝑋) ∈ (Unit‘𝑅) ∧ (𝑋 · 𝑍) = 𝑌)) → 𝑍 = ((𝐼‘𝑋) · 𝑌)) | ||
Theorem | slesolinvbi 22702 | The solution of a system of linear equations represented by a matrix with a unit as determinant is the multiplication of the inverse of the matrix with the right-hand side vector. (Contributed by AV, 11-Feb-2019.) (Revised by AV, 28-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐼 = (invr‘𝐴) ⇒ ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((𝑋 · 𝑍) = 𝑌 ↔ 𝑍 = ((𝐼‘𝑋) · 𝑌))) | ||
Theorem | slesolex 22703* | Every system of linear equations represented by a matrix with a unit as determinant has a solution. (Contributed by AV, 11-Feb-2019.) (Revised by AV, 28-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐷 = (𝑁 maDet 𝑅) ⇒ ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ∃𝑧 ∈ 𝑉 (𝑋 · 𝑧) = 𝑌) | ||
Theorem | cramerimplem1 22704 | Lemma 1 for cramerimp 22707: The determinant of the identity matrix with the ith column replaced by a (column) vector equals the ith component of the vector. (Contributed by AV, 15-Feb-2019.) (Revised by AV, 5-Jul-2022.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) & ⊢ 𝐷 = (𝑁 maDet 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐷‘𝐸) = (𝑍‘𝐼)) | ||
Theorem | cramerimplem2 22705 | Lemma 2 for cramerimp 22707: The matrix of a system of linear equations multiplied with the identity matrix with the ith column replaced by the solution vector of the system of linear equations equals the matrix of the system of linear equations with the ith column replaced by the right-hand side vector of the system of linear equations. (Contributed by AV, 19-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) & ⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ × = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋 × 𝐸) = 𝐻) | ||
Theorem | cramerimplem3 22706 | Lemma 3 for cramerimp 22707: The determinant of the matrix of a system of linear equations multiplied with the determinant of the identity matrix with the ith column replaced by the solution vector of the system of linear equations equals the determinant of the matrix of the system of linear equations with the ith column replaced by the right-hand side vector of the system of linear equations. (Contributed by AV, 19-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) & ⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ ⊗ = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)) = (𝐷‘𝐻)) | ||
Theorem | cramerimp 22707 | One direction of Cramer's rule (according to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule: "[Cramer's rule] ... expresses the solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations."): The ith component of the solution vector of a system of linear equations equals the determinant of the matrix of the system of linear equations with the ith column replaced by the righthand side vector of the system of linear equations divided by the determinant of the matrix of the system of linear equations. (Contributed by AV, 19-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) & ⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝑋 · 𝑍) = 𝑌 ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅))) → (𝑍‘𝐼) = ((𝐷‘𝐻) / (𝐷‘𝑋))) | ||
Theorem | cramerlem1 22708* | Lemma 1 for cramer 22712. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝐷‘𝑋) ∈ (Unit‘𝑅) ∧ 𝑍 ∈ 𝑉 ∧ (𝑋 · 𝑍) = 𝑌)) → 𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋)))) | ||
Theorem | cramerlem2 22709* | Lemma 2 for cramer 22712. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ∀𝑧 ∈ 𝑉 ((𝑋 · 𝑧) = 𝑌 → 𝑧 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))))) | ||
Theorem | cramerlem3 22710* | Lemma 3 for cramer 22712. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) | ||
Theorem | cramer0 22711* | Special case of Cramer's rule for 0-dimensional matrices/vectors. (Contributed by AV, 28-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) | ||
Theorem | cramer 22712* | Cramer's rule. According to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule: "[Cramer's rule] ... expresses the [unique] solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations." If it is assumed that a (unique) solution exists, it can be obtained by Cramer's rule (see also cramerimp 22707). On the other hand, if a vector can be constructed by Cramer's rule, it is a solution of the system of linear equations, so at least one solution exists. The uniqueness is ensured by considering only systems of linear equations whose matrix has a unit (of the underlying ring) as determinant, see matunit 22699 or slesolinv 22701. For fields as underlying rings, this requirement is equivalent to the determinant not being 0. Theorem 4.4 in [Lang] p. 513. This is Metamath 100 proof #97. (Contributed by Alexander van der Vekens, 21-Feb-2019.) (Revised by Alexander van der Vekens, 1-Mar-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ (𝑋 · 𝑍) = 𝑌)) | ||
A polynomial matrix or matrix of polynomials is a matrix whose elements are univariate (or multivariate) polynomials. See Wikipedia "Polynomial matrix" https://en.wikipedia.org/wiki/Polynomial_matrix (18-Nov-2019). In this section, only square matrices whose elements are univariate polynomials are considered. Usually, the ring of such matrices, the ring of n x n matrices over the polynomial ring over a ring 𝑅, is denoted by M(n, R[t]). The elements of this ring are called "polynomial matrices (over the ring 𝑅)" in the following. In Metamath notation, this ring is defined by (𝑁 Mat (Poly1‘𝑅)), usually represented by the class variable 𝐶 (or 𝑌, if 𝐶 is already occupied): 𝐶 = (𝑁 Mat 𝑃) with 𝑃 = (Poly1‘𝑅). | ||
Theorem | pmatring 22713 | The set of polynomial matrices over a ring is a ring. (Contributed by AV, 6-Nov-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) | ||
Theorem | pmatlmod 22714 | The set of polynomial matrices over a ring is a left module. (Contributed by AV, 6-Nov-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ LMod) | ||
Theorem | pmatassa 22715 | The set of polynomial matrices over a commutative ring is an associative algebra. (Contributed by AV, 16-Jun-2024.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ AssAlg) | ||
Theorem | pmat0op 22716* | 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 22717* | 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 22718 | 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 22719* | 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 22720* | 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 22721 | 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 22722* | 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 22723 | 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 21892) 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 22728), 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 22742) 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 22779). Thus, the ring of matrices over a commutative ring is isomorphic to the ring of scalar matrices over the same ring, see matcpmric 22780. Finally, 𝐼 = (𝑁 cPolyMatToMat 𝑅), the transformation of a constant polynomial matrix into a matrix, is the inverse function of the matrix transformation 𝑇 = (𝑁 matToPolyMat 𝑅), see m2cpminv 22781. | ||
Syntax | ccpmat 22724 | Extend class notation with the set of all constant polynomial matrices. |
class ConstPolyMat | ||
Syntax | cmat2pmat 22725 | Extend class notation with the transformation of a matrix into a matrix of polynomials. |
class matToPolyMat | ||
Syntax | ccpmat2mat 22726 | Extend class notation with the transformation of a constant polynomial matrix into a matrix. |
class cPolyMatToMat | ||
Definition | df-cpmat 22727* | The set of all constant polynomial matrices, which are all matrices whose entries are constant polynomials (or "scalar polynomials", see ply1sclf 22303). (Contributed by AV, 15-Nov-2019.) |
⊢ ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)}) | ||
Definition | df-mat2pmat 22728* | 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 22729* | 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 22781, it is also called "inverse matrix transformation" in the following. (Contributed by AV, 14-Dec-2019.) |
⊢ cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))) | ||
Theorem | cpmat 22730* | 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 22731 | A constant polynomial matrix is a polynomial matrix. (Contributed by AV, 16-Nov-2019.) |
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) → 𝑀 ∈ 𝐵) | ||
Theorem | cpmatel 22732* | Property of a constant polynomial matrix. (Contributed by AV, 15-Nov-2019.) |
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑀 ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅))) | ||
Theorem | cpmatelimp 22733* | 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 22734* | 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 22735* | 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 22736 | 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 22737* | 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 22738* | 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 22739* | Lemma for cpmatmcl 22740. (Contributed by AV, 18-Nov-2019.) |
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑐 ∈ ℕ ((coe1‘(𝑃 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑥𝑘)(.r‘𝑃)(𝑘𝑦𝑗)))))‘𝑐) = (0g‘𝑅)) | ||
Theorem | cpmatmcl 22740* | 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 22741 | 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 22742 | 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 22743 | 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 22744* | Value of the matrix transformation. (Contributed by AV, 31-Jul-2019.) |
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦))))) | ||
Theorem | mat2pmatval 22745* | The result of a matrix transformation. (Contributed by AV, 31-Jul-2019.) |
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑀𝑦)))) | ||
Theorem | mat2pmatvalel 22746 | A (matrix) element of the result of a matrix transformation. (Contributed by AV, 31-Jul-2019.) |
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (𝑋(𝑇‘𝑀)𝑌) = (𝑆‘(𝑋𝑀𝑌))) | ||
Theorem | mat2pmatbas 22747 | 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 22748 | 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 22749 | 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 22750 | 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 22751 | 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 22752* | 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 22753 | 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 22754 | 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 22755 | 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 22756 | The transformation of matrices into polynomial matrices is "linear", analogous to lmhmlin 21051. Since 𝐴 and 𝐶 have different scalar rings, 𝑇 cannot be a left module homomorphism as defined in df-lmhm 21038, see lmhmsca 21046. (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 22757 | 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 22758 | 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 22759 | 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 22760 | The transformation of a matrix of dimenson 1. (Contributed by AV, 4-Aug-2019.) |
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉}) | ||
Theorem | mat2pmatscmxcl 22761 | 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 22762 | 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 22763 | 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 22764 | 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 22765 | 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 22766 | 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 22767 | 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 22768 | 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 22769* | 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 22770* | Value of the inverse matrix transformation. (Contributed by AV, 14-Dec-2019.) |
⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅) & ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐼 = (𝑚 ∈ 𝑆 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))) | ||
Theorem | cpm2mval 22771* | 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 22772 | A (matrix) element of the result of an inverse matrix transformation. (Contributed by AV, 14-Dec-2019.) |
⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅) & ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (𝑋(𝐼‘𝑀)𝑌) = ((coe1‘(𝑋𝑀𝑌))‘0)) | ||
Theorem | cpm2mf 22773 | 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 22774 | 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 22775* | Lemma for m2cpminvid2 22776. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.) |
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑛 ∈ ℕ0 ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) | ||
Theorem | m2cpminvid2 22776 | 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 22777 | 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 22778 | 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 22779 | 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 22780 | 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 22781 | 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 22782 | 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 22784), 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 22802. | ||
Syntax | cdecpmat 22783 | Extend class notation to include the decomposition of polynomial matrices. |
class decompPMat | ||
Definition | df-decpmat 22784* | 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 22785* | 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 22786* | 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 22787 | 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 22788 | 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 22789* | 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 22790* | 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 22791 | 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 22792* | Lemma for decpmatmul 22793. (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 22793* | 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 22794* | Lemma 0 for pm2mpmhm 22841. (Contributed by AV, 21-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ · = (.r‘𝐴) & ⊢ 0 = (0g‘𝐴) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑙 ∈ ℕ0 ↦ (𝐴 Σg (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑙 − 𝑘)))))) finSupp 0 ) | ||
Theorem | pmatcollpw1lem1 22795* | Lemma 1 for pmatcollpw1 22797. (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 22796* | Lemma 2 for pmatcollpw1 22797: 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 22797* | 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 22798* | Lemma for pmatcollpw2 22799. (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 22799* | 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 22800 | 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 22791 (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 )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |