Home | Metamath
Proof Explorer Theorem List (p. 213 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | smadiadetlem1 21201* | Lemma 1 for smadiadet 21209: A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-Jan-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) ∧ 𝑝 ∈ 𝑃) → (((𝑌 ∘ 𝑆)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗)))(𝑝‘𝑛))))) ∈ (Base‘𝑅)) | ||
Theorem | smadiadetlem1a 21202* | Lemma 1a for smadiadet 21209: The summands of the Leibniz' formula vanish for all permutations fixing the index of the row containing the 0's and the 1 to the column with the 1. (Contributed by AV, 3-Jan-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑅 Σg (𝑝 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗)))(𝑝‘𝑛))))))) = 0 ) | ||
Theorem | smadiadetlem2 21203* | Lemma 2 for smadiadet 21209: The summands of the Leibniz' formula vanish for all permutations fixing the index of the row containing the 0's and the 1 to itself. (Contributed by AV, 31-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑅 Σg (𝑝 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗)))(𝑝‘𝑛))))))) = 0 ) | ||
Theorem | smadiadetlem3lem0 21204* | Lemma 0 for smadiadetlem3 21207. (Contributed by AV, 12-Jan-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑊 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾})) ⇒ ⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ 𝑊) → (((𝑌 ∘ 𝑍)‘𝑄)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑄‘𝑛))))) ∈ (Base‘𝑅)) | ||
Theorem | smadiadetlem3lem1 21205* | Lemma 1 for smadiadetlem3 21207. (Contributed by AV, 12-Jan-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑊 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾})) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))):𝑊⟶(Base‘𝑅)) | ||
Theorem | smadiadetlem3lem2 21206* | Lemma 2 for smadiadetlem3 21207. (Contributed by AV, 12-Jan-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑊 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾})) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → ran (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) ⊆ ((Cntz‘𝑅)‘ran (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))))) | ||
Theorem | smadiadetlem3 21207* | Lemma 3 for smadiadet 21209. (Contributed by AV, 31-Jan-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑊 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾})) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑅 Σg (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (((𝑌 ∘ 𝑆)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))))))) = (𝑅 Σg (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))))) | ||
Theorem | smadiadetlem4 21208* | Lemma 4 for smadiadet 21209. (Contributed by AV, 31-Jan-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑊 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾})) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑅 Σg (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (((𝑌 ∘ 𝑆)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗)))(𝑝‘𝑛))))))) = (𝑅 Σg (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))))) | ||
Theorem | smadiadet 21209 | The determinant of a submatrix of a square matrix obtained by removing a row and a column at the same index equals the determinant of the original matrix with the row replaced with 0's and a 1 at the diagonal position. (Contributed by AV, 31-Jan-2019.) (Proof shortened by AV, 24-Jul-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐸 = ((𝑁 ∖ {𝐾}) maDet 𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝐸‘(𝐾((𝑁 subMat 𝑅)‘𝑀)𝐾)) = (𝐷‘(𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾))) | ||
Theorem | smadiadetglem1 21210 | Lemma 1 for smadiadetg 21212. (Contributed by AV, 13-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐸 = ((𝑁 ∖ {𝐾}) maDet 𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = ((𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁))) | ||
Theorem | smadiadetglem2 21211 | Lemma 2 for smadiadetg 21212. (Contributed by AV, 14-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐸 = ((𝑁 ∖ {𝐾}) maDet 𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) ↾ ({𝐾} × 𝑁)) = ((({𝐾} × 𝑁) × {𝑆}) ∘f · ((𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾) ↾ ({𝐾} × 𝑁)))) | ||
Theorem | smadiadetg 21212 | The determinant of a square matrix with one row replaced with 0's and an arbitrary element of the underlying ring at the diagonal position equals the ring element multiplied with the determinant of a submatrix of the square matrix obtained by removing the row and the column at the same index. (Contributed by AV, 14-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐸 = ((𝑁 ∖ {𝐾}) maDet 𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → (𝐷‘(𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾)) = (𝑆 · (𝐸‘(𝐾((𝑁 subMat 𝑅)‘𝑀)𝐾)))) | ||
Theorem | smadiadetg0 21213 | Lemma for smadiadetr 21214: version of smadiadetg 21212 with all hypotheses defining class variables removed, i.e. all class variables defined in the hypotheses replaced in the theorem by their definition. (Contributed by AV, 15-Feb-2019.) |
⊢ 𝑅 ∈ CRing ⇒ ⊢ ((𝑀 ∈ (Base‘(𝑁 Mat 𝑅)) ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝑁 maDet 𝑅)‘(𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾)) = (𝑆(.r‘𝑅)(((𝑁 ∖ {𝐾}) maDet 𝑅)‘(𝐾((𝑁 subMat 𝑅)‘𝑀)𝐾)))) | ||
Theorem | smadiadetr 21214 | The determinant of a square matrix with one row replaced with 0's and an arbitrary element of the underlying ring at the diagonal position equals the ring element multiplied with the determinant of a submatrix of the square matrix obtained by removing the row and the column at the same index. Closed form of smadiadetg 21212. Special case of the "Laplace expansion", see definition in [Lang] p. 515. (Contributed by AV, 15-Feb-2019.) |
⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝑁 Mat 𝑅))) ∧ (𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅))) → ((𝑁 maDet 𝑅)‘(𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾)) = (𝑆(.r‘𝑅)(((𝑁 ∖ {𝐾}) maDet 𝑅)‘(𝐾((𝑁 subMat 𝑅)‘𝑀)𝐾)))) | ||
Theorem | invrvald 21215 | If a matrix multiplied with a given matrix (from the left as well as from the right) results in the identity matrix, this matrix is the inverse (matrix) of the given matrix. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 · 𝑌) = 1 ) & ⊢ (𝜑 → (𝑌 · 𝑋) = 1 ) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ∧ (𝐼‘𝑋) = 𝑌)) | ||
Theorem | matinv 21216 | The inverse of a matrix is the adjunct of the matrix multiplied with the inverse of the determinant of the matrix if the determinant is a unit in the underlying ring. Proposition 4.16 in [Lang] p. 518. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐽 = (𝑁 maAdju 𝑅) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑈 = (Unit‘𝐴) & ⊢ 𝑉 = (Unit‘𝑅) & ⊢ 𝐻 = (invr‘𝑅) & ⊢ 𝐼 = (invr‘𝐴) & ⊢ ∙ = ( ·𝑠 ‘𝐴) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ (𝐷‘𝑀) ∈ 𝑉) → (𝑀 ∈ 𝑈 ∧ (𝐼‘𝑀) = ((𝐻‘(𝐷‘𝑀)) ∙ (𝐽‘𝑀)))) | ||
Theorem | matunit 21217 | A matrix is a unit in the ring of matrices iff its determinant is a unit in the underlying ring. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑈 = (Unit‘𝐴) & ⊢ 𝑉 = (Unit‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑀 ∈ 𝑈 ↔ (𝐷‘𝑀) ∈ 𝑉)) | ||
In the following, Cramer's rule cramer 21230 is proven. According to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule 21230: "[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." The outline of the proof for systems of linear equations with coefficients from a commutative ring, according to the proof in Wikipedia (https://en.wikipedia.org/wiki/Cramer's_rule#A_short_proof), 21230 is as follows: The system of linear equations 𝐴 × 𝑋 = 𝐵 to be solved shall be given by the N x N coefficient matrix 𝐴 and the N-dimensional vector 𝐵. Let (𝐴‘𝑖) be the matrix obtained by replacing the i-th column of the coefficient matrix 𝐴 by the right-hand side vector 𝐵. Additionally, let (𝑋‘𝑖) be the matrix obtained by replacing the i-th column of the identity matrix by the solution vector 𝑋, with 𝑋 = (𝑥‘𝑖). Finally, it is assumed that det 𝐴 is a unit in the underlying ring. With these definitions, it follows that 𝐴 × (𝑋‘𝑖) = (𝐴‘𝑖) (cramerimplem2 21223), using matrix multiplication (mamuval 20927) and multiplication of a vector with a matrix (mulmarep1gsum2 21113). By using the multiplicativity of the determinant (mdetmul 21162) it follows that det (𝐴‘𝑖) = det (𝐴 × (𝑋‘𝑖)) = det 𝐴 · det (𝑋‘𝑖) (cramerimplem3 21224). Furthermore, it follows that det (𝑋‘𝑖) = (𝑥‘𝑖) (cramerimplem1 21222). To show this, a special case of the Laplace expansion is used (smadiadetg 21212). From these equations and the cancellation law for division in a ring (dvrcan3 19373) it follows that (𝑥‘𝑖) = det (𝑋‘𝑖) = det (𝐴‘𝑖) / det 𝐴. This is the right to left implication (cramerimp 21225, cramerlem1 21226, cramerlem2 21227) of Cramer's rule (cramer 21230). The left to right implication is shown by cramerlem3 21228, using the fact that a solution of the system of linear equations exists (slesolex 21221). Notice that for the special case of 0-dimensional matrices/vectors only the left to right implication is valid (see cramer0 21229), because assuming the right-hand side of the implication ((𝑋 · 𝑍) = 𝑌), 𝑍 could be anything (see mavmul0g 21092). | ||
Theorem | slesolvec 21218 | Every solution of a system of linear equations represented by a matrix and a vector is a vector. (Contributed by AV, 10-Feb-2019.) (Revised by AV, 27-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) ⇒ ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉)) | ||
Theorem | slesolinv 21219 | 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 21220 | 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 21221* | 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 21222 | Lemma 1 for cramerimp 21225: 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 21223 | Lemma 2 for cramerimp 21225: 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 21224 | Lemma 3 for cramerimp 21225: 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 21225 | 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 21226* | Lemma 1 for cramer 21230. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝐷‘𝑋) ∈ (Unit‘𝑅) ∧ 𝑍 ∈ 𝑉 ∧ (𝑋 · 𝑍) = 𝑌)) → 𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋)))) | ||
Theorem | cramerlem2 21227* | Lemma 2 for cramer 21230. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ∀𝑧 ∈ 𝑉 ((𝑋 · 𝑧) = 𝑌 → 𝑧 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))))) | ||
Theorem | cramerlem3 21228* | Lemma 3 for cramer 21230. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) | ||
Theorem | cramer0 21229* | 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 21230* | 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 21225). 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 21217 or slesolinv 21219. 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 21231 | The set of polynomial matrices over a ring is a ring. (Contributed by AV, 6-Nov-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) | ||
Theorem | pmatlmod 21232 | The set of polynomial matrices over a ring is a left module. (Contributed by AV, 6-Nov-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ LMod) | ||
Theorem | pmat0op 21233* | 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 21234* | 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 21235 | 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 21236* | The zero polynomial matrix over a ring represented as operation with "lifted scalars" (i.e. elements of the ring underlying the polynomial ring embedded into the polynomial ring by the scalar injection/algebraic scalars function algSc). (Contributed by AV, 16-Nov-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝐴‘ 0 ))) | ||
Theorem | pmat1opsc 21237* | 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 21238 | 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 21239* | 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 21240 | 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 20017) to a scalar 𝐴 ∈ 𝑅: ((algSc‘𝑃)‘𝐴). In an analogous way, constant polynomial matrices (over the ring 𝑅) are obtained by "lifting" matrices over the ring 𝑅 by the function matToPolyMat (see df-mat2pmat 21245), 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 21259) and that 𝑇 = (𝑁 matToPolyMat 𝑅) is a ring isomorphism between the ring of matrices over a ring 𝑅 and the ring of constant polynomial matrices over the ring 𝑅 (see m2cpmrngiso 21296). By this, it is shown that the ring of matrices over a commutative ring is isomorphic to the ring of scalar matrices over the same ring, see matcpmric 21297. Finally 𝐼 = (𝑁 cPolyMatToMat 𝑅), the transformation of a constant polynomial matrix into a matrix, is the inverse function of the matrix transformation 𝑇 = (𝑁 matToPolyMat 𝑅), see m2cpminv 21298. | ||
Syntax | ccpmat 21241 | Extend class notation with the set of all constant polynomial matrices. |
class ConstPolyMat | ||
Syntax | cmat2pmat 21242 | Extend class notation with the transformation of a matrix into a matrix of polynomials. |
class matToPolyMat | ||
Syntax | ccpmat2mat 21243 | Extend class notation with the transformation of a constant polynomial matrix into a matrix. |
class cPolyMatToMat | ||
Definition | df-cpmat 21244* | The set of all constant polynomial matrices, which are all matrices whose entries are constant polynomials (or "scalar polynomials", see ply1sclf 20383). (Contributed by AV, 15-Nov-2019.) |
⊢ ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)}) | ||
Definition | df-mat2pmat 21245* | 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 21246* | 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 21298, it is also called "inverse matrix transformation" in the following. (Contributed by AV, 14-Dec-2019.) |
⊢ cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))) | ||
Theorem | cpmat 21247* | 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 21248 | A constant polynomial matrix is a polynomial matrix. (Contributed by AV, 16-Nov-2019.) |
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) → 𝑀 ∈ 𝐵) | ||
Theorem | cpmatel 21249* | Property of a constant polynomial matrix. (Contributed by AV, 15-Nov-2019.) |
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑀 ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅))) | ||
Theorem | cpmatelimp 21250* | 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 21251* | 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 21252* | 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 21253 | 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 21254* | 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 21255* | 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 21256* | Lemma for cpmatmcl 21257. (Contributed by AV, 18-Nov-2019.) |
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑐 ∈ ℕ ((coe1‘(𝑃 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑥𝑘)(.r‘𝑃)(𝑘𝑦𝑗)))))‘𝑐) = (0g‘𝑅)) | ||
Theorem | cpmatmcl 21257* | 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 21258 | 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 21259 | 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 21260 | 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 21261* | Value of the matrix transformation. (Contributed by AV, 31-Jul-2019.) |
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦))))) | ||
Theorem | mat2pmatval 21262* | The result of a matrix transformation. (Contributed by AV, 31-Jul-2019.) |
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑀𝑦)))) | ||
Theorem | mat2pmatvalel 21263 | A (matrix) element of the result of a matrix transformation. (Contributed by AV, 31-Jul-2019.) |
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (𝑋(𝑇‘𝑀)𝑌) = (𝑆‘(𝑋𝑀𝑌))) | ||
Theorem | mat2pmatbas 21264 | 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 21265 | 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 21266 | 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 21267 | 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 21268 | 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 21269* | 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 21270 | 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 21271 | 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 21272 | 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 21273 | The transformation of matrices into polynomial matrices is "linear", analogous to lmhmlin 19738. Since 𝐴 and 𝐶 have different scalar rings, 𝑇 cannot be a left module homomorphism as defined in df-lmhm 19725, see lmhmsca 19733. (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 21274 | 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 21275 | 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 21276 | 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 21277 | The transformation of a matrix of dimenson 1. (Contributed by AV, 4-Aug-2019.) |
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉}) | ||
Theorem | mat2pmatscmxcl 21278 | 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 21279 | 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 21280 | 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 21281 | 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 21282 | 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 21283 | 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 21284 | 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 21285 | 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 21286* | 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 21287* | Value of the inverse matrix transformation. (Contributed by AV, 14-Dec-2019.) |
⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅) & ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐼 = (𝑚 ∈ 𝑆 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))) | ||
Theorem | cpm2mval 21288* | 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 21289 | A (matrix) element of the result of an inverse matrix transformation. (Contributed by AV, 14-Dec-2019.) |
⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅) & ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁)) → (𝑋(𝐼‘𝑀)𝑌) = ((coe1‘(𝑋𝑀𝑌))‘0)) | ||
Theorem | cpm2mf 21290 | 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 21291 | 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 21292* | Lemma for m2cpminvid2 21293. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 14-Dec-2019.) |
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑛 ∈ ℕ0 ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) | ||
Theorem | m2cpminvid2 21293 | 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 21294 | 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 21295 | 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 21296 | 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 21297 | 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 21298 | 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 21299 | 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 functiondecompPMat (see df-decpmat 21301), 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 21319. | ||
Syntax | cdecpmat 21300 | Extend class notation to include the decomposition of polynomial matrices. |
class decompPMat |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |