![]() |
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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpw2 22501* | Write a polynomial matrix as a sum of matrices whose entries are products of variable powers and constant polynomials collecting like powers. (Contributed by AV, 3-Oct-2019.) (Revised by AV, 3-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΅ = (BaseβπΆ) & β’ Γ = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) β β’ ((π β Fin β§ π β Ring β§ π β π΅) β π = (πΆ Ξ£g (π β β0 β¦ (π β π, π β π β¦ ((π(π decompPMat π)π) Γ (π β π)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | monmatcollpw 22502 | 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 22493 (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 22503 | Lemma for pmatcollpw 22504. (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 22504* | 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 22505* | 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 22506* | Lemma for pmatcollpw3 22507 and pmatcollpw3fi 22508: 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 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, 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 22508* | 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 22509* | Lemma 1 for pmatcollpw3fi1 22511. (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 22510* | Lemma 2 for pmatcollpw3fi1 22511. (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 22511* | 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 22512 | Lemma 1 for pmatcollpwscmat 22514. (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 22513 | Lemma 2 for pmatcollpwscmat 22514. (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 22514* | 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 22546, 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 22515 | Extend class notation with the transformation of a polynomial matrix into a polynomial over matrices. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class pMatToMatPoly | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-pm2mp 22516* | 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 22517* | Lemma for pm2mpf1 22522. (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 22518* | 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 22519* | 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 22520 | 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 22521 | 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 22522 | 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 22523 | 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 22524 | 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 22525* | 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 22526* | Lemma for mply1topmatcl 22528. (Contributed by AV, 6-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) β β’ (((π β Fin β§ π β Ring β§ π β πΏ) β§ πΌ β π β§ π½ β π) β (π β β0 β¦ ((πΌ((coe1βπ)βπ)π½) Β· (ππΈπ))) finSupp (0gβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mply1topmatval 22527* | 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 22534). (Contributed by AV, 6-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ πΏ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (var1βπ ) & β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) β β’ ((π β π β§ π β πΏ) β (πΌβπ) = (π β π, π β π β¦ (π Ξ£g (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mply1topmatcl 22528* | 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 22529* | Lemma 1 for mp2pm2mp 22534. (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 22530* | Lemma 2 for mp2pm2mp 22534. (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 22531* | Lemma 3 for mp2pm2mp 22534. (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 22532* | Lemma 4 for mp2pm2mp 22534. (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 22533* | Lemma 5 for mp2pm2mp 22534. (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 22534* | 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 22535* | Lemma 2 for pm2mpghm 22539. (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 22536 | 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 22537 | 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 22538 | 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 22539 | 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 22540 | 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 22541* | Lemma 1 for pm2mpmhm 22543. (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 22542* | Lemma 2 for pm2mpmhm 22543. (Contributed by AV, 22-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = (Poly1βπ ) & β’ πΆ = (π Mat π) & β’ π΄ = (π Mat π ) & β’ π = (Poly1βπ΄) & β’ π = (π pMatToMatPoly π ) & β’ π΅ = (BaseβπΆ) β β’ ((π β Fin β§ π β Ring) β βπ₯ β π΅ βπ¦ β π΅ (πβ(π₯(.rβπΆ)π¦)) = ((πβπ₯)(.rβπ)(πβπ¦))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpmhm 22543 | 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 22544 | 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 22545 | 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 22546 | 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 22547 | 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 22548* | 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 22550) the eigenvalues and corresponding eigenvectors can be defined. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
The characteristic polynomial of a matrix π΄ is the determinant of the characteristic matrix of π΄: (π‘πΌ β π΄). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cchpmat 22549 | Extend class notation with the characteristic polynomial. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class CharPlyMat | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-chpmat 22550* | 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 22551 | 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 22552 | 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 22553* | 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 22554 | 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 22555 | 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 22556* | 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 22557 | The characteristic polynomial of the empty matrix. (Contributed by AV, 6-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (β CharPlyMat π ) β β’ (π β Ring β (πΆββ ) = (1rβ(Poly1βπ ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat1dlem 22558 | Lemma for chpmat1d 22559. (Contributed by AV, 7-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (var1βπ ) & β’ β = (-gβπ) & β’ π = (algScβπ) & β’ πΊ = (π Mat π) & β’ π = (π matToPolyMat π ) β β’ ((π β Ring β§ (π = {πΌ} β§ πΌ β π) β§ π β π΅) β (πΌ((π( Β·π βπΊ)(1rβπΊ))(-gβπΊ)(πβπ))πΌ) = (π β (πβ(πΌππΌ)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat1d 22559 | 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 22560 | Lemma 0 for chpdmat 22564. (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 22561 | Lemma 1 for chpdmat 22564. (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 22562 | Lemma 2 for chpdmat 22564. (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 22563 | Lemma 3 for chpdmat 22564. (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 22564* | 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 22565* | 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 22566* | 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 22567* | 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 22568* | 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 22569 | 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 22570 | 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 22571 | 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 22601. 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 22589, cayhamlem3 22610 and cayhamlem4 22611. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04if 22572* | 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 22573* | 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 22574* | 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 22575* | 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 22576* | 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 22577* | 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 22578* | 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 22579* | 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 22580* | 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 22581* | 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 22582* | 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 22583* | 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 22584* | 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 22585* | 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 22586* | 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 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) β (πβπ)) Γ (πβ(πβπ ))) β ((πβπ) Γ (πβ(πβ0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulgsum2 22588* | 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 22589* | Lemma 1 for cayleyhamilton 22613. (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 22590 | The right-hand fundamental relation of the adjugate (see madurid 22367) 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 22591* | 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 22592* | 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 22593* | Lemma 1 for cpmidpmat 22596. (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 22594* | Lemma 2 for cpmidpmat 22596. (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 22595* | Lemma 3 for cpmidpmat 22596. (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 22596* | 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 22597* | Lemma B for cpmadugsum 22601. (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 22598* | Lemma C for cpmadugsum 22601. (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 22599* | Lemma F for cpmadugsum 22601. (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 22600* | 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)))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |