![]() |
Metamath
Proof Explorer Theorem List (p. 226 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | monmatcollpw 22501 | 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 22492 (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 22502 | Lemma for pmatcollpw 22503. (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 22503* | 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 22504* | 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 22505* | Lemma for pmatcollpw3 22506 and pmatcollpw3fi 22507: 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 22506* | 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 22507* | 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 22508* | Lemma 1 for pmatcollpw3fi1 22510. (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 22509* | Lemma 2 for pmatcollpw3fi1 22510. (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 22510* | 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 22511 | Lemma 1 for pmatcollpwscmat 22513. (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 22512 | Lemma 2 for pmatcollpwscmat 22513. (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 22513* | 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 22545, 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 22514 | Extend class notation with the transformation of a polynomial matrix into a polynomial over matrices. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class pMatToMatPoly | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-pm2mp 22515* | 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 22516* | Lemma for pm2mpf1 22521. (Contributed by AV, 14-Oct-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) β β’ (((π β Fin β§ π β Ring) β§ (π β π΅ β§ πΎ β β0)) β ((coe1β(π Ξ£g (π β β0 β¦ ((π decompPMat π) β (π β π)))))βπΎ) = (π decompPMat πΎ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpval 22517* | Value of the transformation of a polynomial matrix into a polynomial over matrices. (Contributed by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β π) β π = (π β π΅ β¦ (π Ξ£g (π β β0 β¦ ((π decompPMat π) β (π β π)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpfval 22518* | A polynomial matrix transformed into a polynomial over matrices. (Contributed by AV, 4-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β π β§ π β π΅) β (πβπ) = (π Ξ£g (π β β0 β¦ ((π decompPMat π) β (π β π))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpcl 22519 | The transformation of polynomial matrices into polynomials over matrices maps polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) & β’ πΏ = (Baseβπ) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β (πβπ) β πΏ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpf 22520 | The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) & β’ πΏ = (Baseβπ) β β’ ((π β Fin β§ π β Ring) β π:π΅βΆπΏ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpf1 22521 | The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 14-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) & β’ πΏ = (Baseβπ) β β’ ((π β Fin β§ π β Ring) β π:π΅β1-1βπΏ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpcoe1 22522 | A coefficient of the polynomial over matrices which is the result of the transformation of a polynomial matrix is the matrix consisting of the coefficients in the polynomial entries of the polynomial matrix. (Contributed by AV, 20-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ (((π β Fin β§ π β Ring) β§ (π β π΅ β§ πΎ β β0)) β ((coe1β(πβπ))βπΎ) = (π decompPMat πΎ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | idpm2idmp 22523 | The transformation of the identity polynomial matrix into polynomials over matrices results in the identity of the polynomials over matrices. (Contributed by AV, 18-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β (πβ(1rβπΆ)) = (1rβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mptcoe1matfsupp 22524* | The mapping extracting the entries of the coefficient matrices of a polynomial over matrices at a fixed position is finitely supported. (Contributed by AV, 6-Oct-2019.) (Proof shortened by AV, 23-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) β β’ (((π β Fin β§ π β Ring β§ π β πΏ) β§ πΌ β π β§ π½ β π) β (π β β0 β¦ (πΌ((coe1βπ)βπ)π½)) finSupp (0gβπ )) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mply1topmatcllem 22525* | Lemma for mply1topmatcl 22527. (Contributed by AV, 6-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) β β’ (((π β Fin β§ π β Ring β§ π β πΏ) β§ πΌ β π β§ π½ β π) β (π β β0 β¦ ((πΌ((coe1βπ)βπ)π½) Β· (ππΈπ))) finSupp (0gβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mply1topmatval 22526* | A polynomial over matrices transformed into a polynomial matrix. πΌ is the inverse function of the transformation π of polynomial matrices into polynomials over matrices: (πβ(πΌβπ)) = π) (see mp2pm2mp 22533). (Contributed by AV, 6-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) β β’ ((π β π β§ π β πΏ) β (πΌβπ) = (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mply1topmatcl 22527* | A polynomial over matrices transformed into a polynomial matrix is a polynomial matrix. (Contributed by AV, 6-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) β β’ ((π β Fin β§ π β Ring β§ π β πΏ) β (πΌβπ) β π΅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mplem1 22528* | Lemma 1 for mp2pm2mp 22533. (Contributed by AV, 9-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) β β’ ((π β Fin β§ π β Ring β§ π β πΏ) β (πΌβπ) = (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mplem2 22529* | Lemma 2 for mp2pm2mp 22533. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) & β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) β β’ ((π β Fin β§ π β Ring β§ π β πΏ) β (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ))))) β π΅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mplem3 22530* | Lemma 3 for mp2pm2mp 22533. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) & β’ π = (Poly1βπ ) β β’ (((π β Fin β§ π β Ring β§ π β πΏ) β§ πΎ β β0) β ((πΌβπ) decompPMat πΎ) = (π β π, π β π β¦ ((coe1β(π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))βπΎ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mplem4 22531* | Lemma 4 for mp2pm2mp 22533. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) & β’ π = (Poly1βπ ) β β’ (((π β Fin β§ π β Ring β§ π β πΏ) β§ πΎ β β0) β ((πΌβπ) decompPMat πΎ) = ((coe1βπ)βπΎ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mplem5 22532* | Lemma 5 for mp2pm2mp 22533. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) & β’ π = (Poly1βπ ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) β β’ ((π β Fin β§ π β Ring β§ π β πΏ) β (π β β0 β¦ (((πΌβπ) decompPMat π) β (π β π))) finSupp (0gβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mp 22533* | A polynomial over matrices transformed into a polynomial matrix transformed back into the polynomial over matrices. (Contributed by AV, 12-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) & β’ π = (Poly1βπ ) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring β§ π β πΏ) β (πβ(πΌβπ)) = π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpghmlem2 22534* | Lemma 2 for pm2mpghm 22538. (Contributed by AV, 15-Oct-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β (π β β0 β¦ ((π decompPMat π) β (π β π))) finSupp (0gβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpghmlem1 22535 | Lemma 1 for pm2mpghm . (Contributed by AV, 15-Oct-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) β β’ (((π β Fin β§ π β Ring β§ π β π΅) β§ πΎ β β0) β ((π decompPMat πΎ) β (πΎ β π)) β πΏ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpfo 22536 | The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π:π΅βontoβπΏ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpf1o 22537 | The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 14-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π:π΅β1-1-ontoβπΏ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpghm 22538 | The transformation of polynomial matrices into polynomials over matrices is an additive group homomorphism. (Contributed by AV, 16-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π β (πΆ GrpHom π)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpgrpiso 22539 | The transformation of polynomial matrices into polynomials over matrices is an additive group isomorphism. (Contributed by AV, 17-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π β (πΆ GrpIso π)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpmhmlem1 22540* | Lemma 1 for pm2mpmhm 22542. (Contributed by AV, 21-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (π pMatToMatPoly π ) β β’ (((π β Fin β§ π β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β β0 β¦ ((π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) β (π β π))) finSupp (0gβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpmhmlem2 22541* | Lemma 2 for pm2mpmhm 22542. (Contributed by AV, 22-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) & β’ π΅ = (BaseβπΆ) β β’ ((π β Fin β§ π β Ring) β βπ₯ β π΅ βπ¦ β π΅ (πβ(π₯(.rβπΆ)π¦)) = ((πβπ₯)(.rβπ)(πβπ¦))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpmhm 22542 | The transformation of polynomial matrices into polynomials over matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 22-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π β ((mulGrpβπΆ) MndHom (mulGrpβπ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mprhm 22543 | The transformation of polynomial matrices into polynomials over matrices is a ring homomorphism. (Contributed by AV, 22-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π β (πΆ RingHom π)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mprngiso 22544 | The transformation of polynomial matrices into polynomials over matrices is a ring isomorphism. (Contributed by AV, 22-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β Ring) β π β (πΆ RingIso π)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmmpric 22545 | The ring of polynomial matrices over a ring is isomorphic to the ring of polynomials over matrices of the same dimension over the same ring. (Contributed by AV, 30-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) β β’ ((π β Fin β§ π β Ring) β πΆ βπ π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | monmat2matmon 22546 | The transformation of a polynomial matrix having scaled monomials with the same power as entries into a scaled monomial as a polynomial over matrices. (Contributed by AV, 11-Nov-2019.) (Revised by AV, 7-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ΄) & β’ π = (Poly1βπ΄) & β’ πΌ = (π pMatToMatPoly π ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπΆ) & β’ π = (π matToPolyMat π ) β β’ (((π β Fin β§ π β CRing) β§ (π β πΎ β§ πΏ β β0)) β (πΌβ((πΏπΈπ) Β· (πβπ))) = (π β (πΏ β π))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mp 22547* | The transformation of a sum of matrices having scaled monomials with the same power as entries into a sum of scaled monomials as a polynomial over matrices. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 7-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ΄) & β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ΄) & β’ π = (Poly1βπ΄) & β’ πΌ = (π pMatToMatPoly π ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπΆ) & β’ π = (π matToPolyMat π ) β β’ (((π β Fin β§ π β CRing) β§ (π β (πΎ βm β0) β§ π finSupp (0gβπ΄))) β (πΌβ(πΆ Ξ£g (π β β0 β¦ ((ππΈπ) Β· (πβ(πβπ)))))) = (π Ξ£g (π β β0 β¦ ((πβπ) β (π β π))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
According to Wikipedia ("Characteristic polynomial", 31-Jul-2019, https://en.wikipedia.org/wiki/Characteristic_polynomial): "In linear algebra, the characteristic polynomial of a square matrix is a polynomial which is invariant under matrix similarity and has the eigenvalues as roots. It has the determinant and the trace of the matrix as coefficients.". Based on the definition of the characteristic polynomial of a square matrix (df-chpmat 22549) the eigenvalues and corresponding eigenvectors can be defined. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
The characteristic polynomial of a matrix π΄ is the determinant of the characteristic matrix of π΄: (π‘πΌ β π΄). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cchpmat 22548 | Extend class notation with the characteristic polynomial. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class CharPlyMat | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-chpmat 22549* | Define the characteristic polynomial of a square matrix. According to Wikipedia ("Characteristic polynomial", 31-Jul-2019, https://en.wikipedia.org/wiki/Characteristic_polynomial): "The characteristic polynomial of [an n x n matrix] A, denoted by pA(t), is the polynomial defined by pA ( t ) = det ( t I - A ) where I denotes the n-by-n identity matrix.". In addition, however, the underlying ring must be commutative, see definition in [Lang], p. 561: " Let k be a commutative ring ... Let M be any n x n matrix in k ... We define the characteristic polynomial PM(t) to be the determinant det ( t In - M ) where In is the unit n x n matrix." To be more precise, the matrices A and I on the right hand side are matrices with coefficients of a polynomial ring. Therefore, the original matrix A over a given commutative ring must be transformed into corresponding matrices over the polynomial ring over the given ring. (Contributed by AV, 2-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ CharPlyMat = (π β Fin, π β V β¦ (π β (Baseβ(π Mat π)) β¦ ((π maDet (Poly1βπ))β(((var1βπ)( Β·π β(π Mat (Poly1βπ)))(1rβ(π Mat (Poly1βπ))))(-gβ(π Mat (Poly1βπ)))((π matToPolyMat π)βπ))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chmatcl 22550 | Closure of the characteristic matrix of a matrix. (Contributed by AV, 25-Oct-2019.) (Proof shortened by AV, 29-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ β = (-gβπ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π» = ((π Β· 1 ) β (πβπ)) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β π» β (Baseβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chmatval 22551 | The entries of the characteristic matrix of a matrix. (Contributed by AV, 2-Aug-2019.) (Proof shortened by AV, 10-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ β = (-gβπ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π» = ((π Β· 1 ) β (πβπ)) & β’ βΌ = (-gβπ) & β’ 0 = (0gβπ) β β’ (((π β Fin β§ π β Ring β§ π β π΅) β§ (πΌ β π β§ π½ β π)) β (πΌπ»π½) = if(πΌ = π½, (π βΌ (πΌ(πβπ)π½)), ( 0 βΌ (πΌ(πβπ)π½)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmatfval 22552* | Value of the characteristic polynomial function. (Contributed by AV, 2-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π· = (π maDet π) & β’ β = (-gβπ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (π matToPolyMat π ) & β’ 1 = (1rβπ) β β’ ((π β Fin β§ π β π) β πΆ = (π β π΅ β¦ (π·β((π Β· 1 ) β (πβπ))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmatval 22553 | The characteristic polynomial of a (square) matrix (expressed with a determinant). (Contributed by AV, 2-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π· = (π maDet π) & β’ β = (-gβπ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (π matToPolyMat π ) & β’ 1 = (1rβπ) β β’ ((π β Fin β§ π β π β§ π β π΅) β (πΆβπ) = (π·β((π Β· 1 ) β (πβπ)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmatply1 22554 | The characteristic polynomial of a (square) matrix over a commutative ring is a polynomial, see also the following remark in [Lang], p. 561: "[the characteristic polynomial] is an element of k[t]". (Contributed by AV, 2-Aug-2019.) (Proof shortened by AV, 29-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ πΈ = (Baseβπ) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β (πΆβπ) β πΈ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmatval2 22555* | The characteristic polynomial of a (square) matrix (expressed with the Leibnitz formula for the determinant). (Contributed by AV, 2-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ β = (-gβπ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (π matToPolyMat π ) & β’ 1 = (1rβπ) & β’ πΊ = (SymGrpβπ) & β’ π» = (BaseβπΊ) & β’ π = (β€RHomβπ) & β’ π = (pmSgnβπ) & β’ π = (mulGrpβπ) & β’ Γ = (.rβπ) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β (πΆβπ) = (π Ξ£g (π β π» β¦ (((π β π)βπ) Γ (π Ξ£g (π₯ β π β¦ ((πβπ₯)((π Β· 1 ) β (πβπ))π₯))))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat0d 22556 | The characteristic polynomial of the empty matrix. (Contributed by AV, 6-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (β CharPlyMat π ) β β’ (π β Ring β (πΆββ ) = (1rβ(Poly1βπ ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat1dlem 22557 | Lemma for chpmat1d 22558. (Contributed by AV, 7-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (var1βπ ) & β’ β = (-gβπ) & β’ π = (algScβπ) & β’ πΊ = (π Mat π) & β’ π = (π matToPolyMat π ) β β’ ((π β Ring β§ (π = {πΌ} β§ πΌ β π) β§ π β π΅) β (πΌ((π( Β·π βπΊ)(1rβπΊ))(-gβπΊ)(πβπ))πΌ) = (π β (πβ(πΌππΌ)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat1d 22558 | The characteristic polynomial of a matrix with dimension 1. (Contributed by AV, 7-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (var1βπ ) & β’ β = (-gβπ) & β’ π = (algScβπ) β β’ ((π β CRing β§ (π = {πΌ} β§ πΌ β π) β§ π β π΅) β (πΆβπ) = (π β (πβ(πΌππΌ)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpdmatlem0 22559 | Lemma 0 for chpdmat 22563. (Contributed by AV, 18-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π = (algScβπ) & β’ π΅ = (Baseβπ΄) & β’ π = (var1βπ ) & β’ 0 = (0gβπ ) & β’ πΊ = (mulGrpβπ) & β’ β = (-gβπ) & β’ π = (π Mat π) & β’ 1 = (1rβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β Fin β§ π β Ring) β (π Β· 1 ) β (Baseβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpdmatlem1 22560 | Lemma 1 for chpdmat 22563. (Contributed by AV, 18-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π = (algScβπ) & β’ π΅ = (Baseβπ΄) & β’ π = (var1βπ ) & β’ 0 = (0gβπ ) & β’ πΊ = (mulGrpβπ) & β’ β = (-gβπ) & β’ π = (π Mat π) & β’ 1 = (1rβπ) & β’ Β· = ( Β·π βπ) & β’ π = (-gβπ) & β’ π = (π matToPolyMat π ) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β ((π Β· 1 )π(πβπ)) β (Baseβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpdmatlem2 22561 | Lemma 2 for chpdmat 22563. (Contributed by AV, 18-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π = (algScβπ) & β’ π΅ = (Baseβπ΄) & β’ π = (var1βπ ) & β’ 0 = (0gβπ ) & β’ πΊ = (mulGrpβπ) & β’ β = (-gβπ) & β’ π = (π Mat π) & β’ 1 = (1rβπ) & β’ Β· = ( Β·π βπ) & β’ π = (-gβπ) & β’ π = (π matToPolyMat π ) β β’ ((((((π β Fin β§ π β Ring β§ π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (π((π Β· 1 )π(πβπ))π) = (0gβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpdmatlem3 22562 | Lemma 3 for chpdmat 22563. (Contributed by AV, 18-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π = (algScβπ) & β’ π΅ = (Baseβπ΄) & β’ π = (var1βπ ) & β’ 0 = (0gβπ ) & β’ πΊ = (mulGrpβπ) & β’ β = (-gβπ) & β’ π = (π Mat π) & β’ 1 = (1rβπ) & β’ Β· = ( Β·π βπ) & β’ π = (-gβπ) & β’ π = (π matToPolyMat π ) β β’ (((π β Fin β§ π β Ring β§ π β π΅) β§ πΎ β π) β (πΎ((π Β· 1 )π(πβπ))πΎ) = (π β (πβ(πΎππΎ)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpdmat 22563* | The characteristic polynomial of a diagonal matrix. (Contributed by AV, 18-Aug-2019.) (Proof shortened by AV, 21-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π = (algScβπ) & β’ π΅ = (Baseβπ΄) & β’ π = (var1βπ ) & β’ 0 = (0gβπ ) & β’ πΊ = (mulGrpβπ) & β’ β = (-gβπ) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ βπ β π βπ β π (π β π β (πππ) = 0 )) β (πΆβπ) = (πΊ Ξ£g (π β π β¦ (π β (πβ(πππ)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpscmat 22564* | The characteristic polynomial of a (nonempty!) scalar matrix. (Contributed by AV, 21-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π = (var1βπ ) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π· = {π β (Baseβπ΄) β£ βπ β (Baseβπ )βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ ))} & β’ π = (algScβπ) & β’ β = (-gβπ) β β’ (((π β Fin β§ π β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β (πΆβπ) = ((β―βπ) β (π β (πβπΈ)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpscmat0 22565* | The characteristic polynomial of a (nonempty!) scalar matrix, expressed with its diagonal element. (Contributed by AV, 21-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π = (var1βπ ) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π· = {π β (Baseβπ΄) β£ βπ β (Baseβπ )βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ ))} & β’ π = (algScβπ) & β’ β = (-gβπ) β β’ (((π β Fin β§ π β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = (πΌππΌ))) β (πΆβπ) = ((β―βπ) β (π β (πβ(πΌππΌ))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpscmatgsumbin 22566* | The characteristic polynomial of a (nonempty!) scalar matrix, expressed as finite group sum of binomials. (Contributed by AV, 2-Sep-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π = (var1βπ ) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π· = {π β (Baseβπ΄) β£ βπ β (Baseβπ )βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ ))} & β’ π = (algScβπ) & β’ β = (-gβπ) & β’ πΉ = (.gβπ) & β’ π» = (mulGrpβπ ) & β’ πΈ = (.gβπ») & β’ πΌ = (invgβπ ) & β’ Β· = ( Β·π βπ) β β’ (((π β Fin β§ π β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β (πΆβπ) = (π Ξ£g (π β (0...(β―βπ)) β¦ (((β―βπ)Cπ)πΉ((((β―βπ) β π)πΈ(πΌβ(π½ππ½))) Β· (π β π)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpscmatgsummon 22567* | The characteristic polynomial of a (nonempty!) scalar matrix, expressed as finite group sum of scaled monomials. (Contributed by AV, 2-Sep-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π = (var1βπ ) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π· = {π β (Baseβπ΄) β£ βπ β (Baseβπ )βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ ))} & β’ π = (algScβπ) & β’ β = (-gβπ) & β’ πΉ = (.gβπ) & β’ π» = (mulGrpβπ ) & β’ πΈ = (.gβπ») & β’ πΌ = (invgβπ ) & β’ Β· = ( Β·π βπ) & β’ π = (.gβπ ) β β’ (((π β Fin β§ π β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β (πΆβπ) = (π Ξ£g (π β (0...(β―βπ)) β¦ ((((β―βπ)Cπ)π(((β―βπ) β π)πΈ(πΌβ(π½ππ½)))) Β· (π β π))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chp0mat 22568 | The characteristic polynomial of the zero matrix. (Contributed by AV, 18-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π = (var1βπ ) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ 0 = (0gβπ΄) β β’ ((π β Fin β§ π β CRing) β (πΆβ 0 ) = ((β―βπ) β π)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpidmat 22569 | The characteristic polynomial of the identity matrix. (Contributed by AV, 19-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π = (var1βπ ) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ πΌ = (1rβπ΄) & β’ π = (algScβπ) & β’ 1 = (1rβπ ) & β’ β = (-gβπ) β β’ ((π β Fin β§ π β CRing) β (πΆβπΌ) = ((β―βπ) β (π β (πβ 1 )))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chmaidscmat 22570 | The characteristic polynomial of a matrix multiplied with the identity matrix is a scalar matrix. (Contributed by AV, 30-Oct-2019.) (Revised by AV, 5-Jul-2022.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ πΈ = (Baseβπ) & β’ π = (π Mat π) & β’ πΎ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π = (π ScMat π) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β ((πΆβπ) Β· 1 ) β π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
In this subsection the function πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) is discussed. This function is involved in the representation of the product of the characteristic matrix of a given matrix and its adjunct as an infinite sum, see cpmadugsum 22600. Therefore, this function is called "characteristic factor function" (in short "chfacf") in the following. It plays an important role in the proof of the Cayley-Hamilton theorem, see cayhamlem1 22588, cayhamlem3 22609 and cayhamlem4 22610. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04if 22571* | The function values of a mapping from the nonnegative integers with four distinct cases. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΊ = (π β β0 β¦ if(π = 0, π΄, if(π = π, πΆ, if(π < π, π·, π΅)))) & β’ (π β π β β) & β’ (π β π β β0) & β’ (π β π β π) & β’ ((π β§ π = 0) β π = β¦π / πβ¦π΄) & β’ ((π β§ 0 < π β§ π < π) β π = β¦π / πβ¦π΅) & β’ ((π β§ π = π) β π = β¦π / πβ¦πΆ) & β’ ((π β§ π < π) β π = β¦π / πβ¦π·) β β’ (π β (πΊβπ) = π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04ifa 22572* | The function value of a mapping from the nonnegative integers with four distinct cases for the first case. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΊ = (π β β0 β¦ if(π = 0, π΄, if(π = π, πΆ, if(π < π, π·, π΅)))) & β’ (π β π β β) & β’ (π β π β β0) β β’ ((π β§ π = 0 β§ β¦π / πβ¦π΄ β π) β (πΊβπ) = β¦π / πβ¦π΄) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04ifb 22573* | The function value of a mapping from the nonnegative integers with four distinct cases for the second case. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΊ = (π β β0 β¦ if(π = 0, π΄, if(π = π, πΆ, if(π < π, π·, π΅)))) & β’ (π β π β β) & β’ (π β π β β0) β β’ ((π β§ (0 < π β§ π < π) β§ β¦π / πβ¦π΅ β π) β (πΊβπ) = β¦π / πβ¦π΅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04ifc 22574* | The function value of a mapping from the nonnegative integers with four distinct cases for the third case. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΊ = (π β β0 β¦ if(π = 0, π΄, if(π = π, πΆ, if(π < π, π·, π΅)))) & β’ (π β π β β) & β’ (π β π β β0) β β’ ((π β§ π = π β§ β¦π / πβ¦πΆ β π) β (πΊβπ) = β¦π / πβ¦πΆ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04ifd 22575* | The function value of a mapping from the nonnegative integers with four distinct cases for the forth case. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΊ = (π β β0 β¦ if(π = 0, π΄, if(π = π, πΆ, if(π < π, π·, π΅)))) & β’ (π β π β β) & β’ (π β π β β0) β β’ ((π β§ π < π β§ β¦π / πβ¦π· β π) β (πΊβπ) = β¦π / πβ¦π·) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfisf 22576* | The "characteristic factor function" is a function from the nonnegative integers to polynomial matrices. (Contributed by AV, 8-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) β β’ (((π β Fin β§ π β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β πΊ:β0βΆ(Baseβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfisfcpmat 22577* | The "characteristic factor function" is a function from the nonnegative integers to constant polynomial matrices. (Contributed by AV, 19-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (π ConstPolyMat π ) β β’ (((π β Fin β§ π β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β πΊ:β0βΆπ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacffsupp 22578* | The "characteristic factor function" is finitely supported. (Contributed by AV, 20-Nov-2019.) (Proof shortened by AV, 23-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β πΊ finSupp (0gβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfscmulcl 22579* | Closure of a scaled value of the "characteristic factor function". (Contributed by AV, 9-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π ))) β§ πΎ β β0) β ((πΎ β π) Β· (πΊβπΎ)) β (Baseβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfscmul0 22580* | A scaled value of the "characteristic factor function" is zero almost always. (Contributed by AV, 9-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π ))) β§ πΎ β (β€β₯β(π + 2))) β ((πΎ β π) Β· (πΊβπΎ)) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfscmulfsupp 22581* | A mapping of scaled values of the "characteristic factor function" is finitely supported. (Contributed by AV, 8-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (π β β0 β¦ ((π β π) Β· (πΊβπ))) finSupp 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfscmulgsum 22582* | Breaking up a sum of values of the "characteristic factor function" scaled by a polynomial. (Contributed by AV, 9-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ + = (+gβπ) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (π Ξ£g (π β β0 β¦ ((π β π) Β· (πΊβπ)))) = ((π Ξ£g (π β (1...π ) β¦ ((π β π) Β· ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ))))))) + ((((π + 1) β π) Β· (πβ(πβπ ))) β ((πβπ) Γ (πβ(πβ0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulcl 22583* | Closure of the value of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ β = (.gβ(mulGrpβπ)) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π ))) β§ πΎ β β0) β ((πΎ β (πβπ)) Γ (πΊβπΎ)) β (Baseβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmul0 22584* | The value of the "characteristic factor function" multiplied with a constant polynomial matrix is zero almost always. (Contributed by AV, 23-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ β = (.gβ(mulGrpβπ)) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π ))) β§ πΎ β (β€β₯β(π + 2))) β ((πΎ β (πβπ)) Γ (πΊβπΎ)) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulfsupp 22585* | A mapping of values of the "characteristic factor function" multiplied with a constant polynomial matrix is finitely supported. (Contributed by AV, 23-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ β = (.gβ(mulGrpβπ)) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (π β β0 β¦ ((π β (πβπ)) Γ (πΊβπ))) finSupp 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulgsum 22586* | Breaking up a sum of values of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ β = (.gβ(mulGrpβπ)) & β’ + = (+gβπ) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (π Ξ£g (π β β0 β¦ ((π β (πβπ)) Γ (πΊβπ)))) = ((π Ξ£g (π β (1...π ) β¦ ((π β (πβπ)) Γ ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ))))))) + ((((π + 1) β (πβπ)) Γ (πβ(πβπ ))) β ((πβπ) Γ (πβ(πβ0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulgsum2 22587* | Breaking up a sum of values of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ β = (.gβ(mulGrpβπ)) & β’ + = (+gβπ) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (π Ξ£g (π β β0 β¦ ((π β (πβπ)) Γ (πΊβπ)))) = ((π Ξ£g (π β (1...π ) β¦ (((π β (πβπ)) Γ (πβ(πβ(π β 1)))) β (((π + 1) β (πβπ)) Γ (πβ(πβπ)))))) + ((((π + 1) β (πβπ)) Γ (πβ(πβπ ))) β ((πβπ) Γ (πβ(πβ0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayhamlem1 22588* | Lemma 1 for cayleyhamilton 22612. (Contributed by AV, 11-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ β = (.gβ(mulGrpβπ)) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (π Ξ£g (π β β0 β¦ ((π β (πβπ)) Γ (πΊβπ)))) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
In this section, a direct algebraic proof for the Cayley-Hamilton theorem is
provided, according to Wikipedia ("Cayley-Hamilton theorem", 09-Nov-2019,
https://en.wikipedia.org/wiki/Cayley%E2%80%93Hamilton_theorem, section
"A direct algebraic proof" (this approach is also used for proving Lemma 1.9 in
[Hefferon] p. 427):
Using this notation, we have:
Following the proof shown in Wikipedia, the following steps are performed:
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadurid 22589 | The right-hand fundamental relation of the adjugate (see madurid 22366) applied to the characteristic matrix of a matrix. (Contributed by AV, 25-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (var1βπ ) & β’ π = (π matToPolyMat π ) & β’ β = (-gβπ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ πΌ = ((π Β· 1 ) β (πβπ)) & β’ π½ = (π maAdju π) & β’ Γ = (.rβπ) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β (πΌ Γ (π½βπΌ)) = ((πΆβπ) Β· 1 )) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidgsum 22590* | Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as group sum. (Contributed by AV, 7-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π = (algScβπ) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (πΆβπ) & β’ π» = (πΎ Β· 1 ) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β π» = (π Ξ£g (π β β0 β¦ ((π β π) Β· ((πβ((coe1βπΎ)βπ)) Β· 1 ))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidgsumm2pm 22591* | Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as group sum with a matrix to polynomial matrix transformation. (Contributed by AV, 13-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π = (algScβπ) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (πΆβπ) & β’ π» = (πΎ Β· 1 ) & β’ π = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ π = (π matToPolyMat π ) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β π» = (π Ξ£g (π β β0 β¦ ((π β π) Β· (πβ(((coe1βπΎ)βπ) β π)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidpmatlem1 22592* | Lemma 1 for cpmidpmat 22595. (Contributed by AV, 13-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π = (algScβπ) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (πΆβπ) & β’ π» = (πΎ Β· 1 ) & β’ π = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ (((coe1βπΎ)βπ) β π)) β β’ (πΏ β β0 β (πΊβπΏ) = (((coe1βπΎ)βπΏ) β π)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidpmatlem2 22593* | Lemma 2 for cpmidpmat 22595. (Contributed by AV, 14-Nov-2019.) (Proof shortened by AV, 7-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π = (algScβπ) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (πΆβπ) & β’ π» = (πΎ Β· 1 ) & β’ π = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ (((coe1βπΎ)βπ) β π)) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β πΊ β (π΅ βm β0)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidpmatlem3 22594* | Lemma 3 for cpmidpmat 22595. (Contributed by AV, 14-Nov-2019.) (Proof shortened by AV, 7-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π = (algScβπ) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (πΆβπ) & β’ π» = (πΎ Β· 1 ) & β’ π = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ (((coe1βπΎ)βπ) β π)) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β πΊ finSupp (0gβπ΄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidpmat 22595* | Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as polynomial over the ring of matrices. (Contributed by AV, 14-Nov-2019.) (Revised by AV, 7-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π = (algScβπ) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (πΆβπ) & β’ π» = (πΎ Β· 1 ) & β’ π = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ π = (π matToPolyMat π ) & β’ π = (Baseβπ) & β’ π = (Poly1βπ΄) & β’ π = (var1βπ΄) & β’ β = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ πΌ = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β (πΌβπ») = (π Ξ£g (π β β0 β¦ ((((coe1βπΎ)βπ) β π) β (ππΈπ))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadugsumlemB 22596* | Lemma B for cpmadugsum 22600. (Contributed by AV, 2-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (π matToPolyMat π ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) & β’ 1 = (1rβπ) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β0 β§ π β (π΅ βm (0...π )))) β ((π Β· 1 ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) = (π Ξ£g (π β (0...π ) β¦ (((π + 1) β π) Β· (πβ(πβπ)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadugsumlemC 22597* | Lemma C for cpmadugsum 22600. (Contributed by AV, 2-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (π matToPolyMat π ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) & β’ 1 = (1rβπ) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β0 β§ π β (π΅ βm (0...π )))) β ((πβπ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) = (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· ((πβπ) Γ (πβ(πβπ))))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadugsumlemF 22598* | Lemma F for cpmadugsum 22600. (Contributed by AV, 7-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (π matToPolyMat π ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) & β’ 1 = (1rβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (((π Β· 1 ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) β ((πβπ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))))) = ((π Ξ£g (π β (1...π ) β¦ ((π β π) Β· ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ))))))) + ((((π + 1) β π) Β· (πβ(πβπ ))) β ((πβπ) Γ (πβ(πβ0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadugsumfi 22599* | The product of the characteristic matrix of a given matrix and its adjunct represented as finite sum. (Contributed by AV, 7-Nov-2019.) (Proof shortened by AV, 29-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (π matToPolyMat π ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) & β’ 1 = (1rβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ πΌ = ((π Β· 1 ) β (πβπ)) & β’ π½ = (π maAdju π) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β βπ β β βπ β (π΅ βm (0...π ))(πΌ Γ (π½βπΌ)) = ((π Ξ£g (π β (1...π ) β¦ ((π β π) Β· ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ))))))) + ((((π + 1) β π) Β· (πβ(πβπ ))) β ((πβπ) Γ (πβ(πβ0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadugsum 22600* | The product of the characteristic matrix of a given matrix and its adjunct represented as an infinite sum. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (π matToPolyMat π ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) & β’ 1 = (1rβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ πΌ = ((π Β· 1 ) β (πβπ)) & β’ π½ = (π maAdju π) & β’ 0 = (0gβπ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β βπ β β βπ β (π΅ βm (0...π ))(πΌ Γ (π½βπΌ)) = (π Ξ£g (π β β0 β¦ ((π β π) Β· (πΊβπ))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |