![]() |
Metamath
Proof Explorer Theorem List (p. 224 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpcoe1 22301 | 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 22302 | 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 22303* | 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 22304* | Lemma for mply1topmatcl 22306. (Contributed by AV, 6-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ = (Poly1โ๐ด) & โข ๐ฟ = (Baseโ๐) & โข ๐ = (Poly1โ๐ ) & โข ยท = ( ยท๐ โ๐) & โข ๐ธ = (.gโ(mulGrpโ๐)) & โข ๐ = (var1โ๐ ) โ โข (((๐ โ Fin โง ๐ โ Ring โง ๐ โ ๐ฟ) โง ๐ผ โ ๐ โง ๐ฝ โ ๐) โ (๐ โ โ0 โฆ ((๐ผ((coe1โ๐)โ๐)๐ฝ) ยท (๐๐ธ๐))) finSupp (0gโ๐)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mply1topmatval 22305* | 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 22312). (Contributed by AV, 6-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ = (Poly1โ๐ด) & โข ๐ฟ = (Baseโ๐) & โข ๐ = (Poly1โ๐ ) & โข ยท = ( ยท๐ โ๐) & โข ๐ธ = (.gโ(mulGrpโ๐)) & โข ๐ = (var1โ๐ ) & โข ๐ผ = (๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0 โฆ ((๐((coe1โ๐)โ๐)๐) ยท (๐๐ธ๐)))))) โ โข ((๐ โ ๐ โง ๐ โ ๐ฟ) โ (๐ผโ๐) = (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0 โฆ ((๐((coe1โ๐)โ๐)๐) ยท (๐๐ธ๐)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mply1topmatcl 22306* | 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 22307* | Lemma 1 for mp2pm2mp 22312. (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 22308* | Lemma 2 for mp2pm2mp 22312. (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 22309* | Lemma 3 for mp2pm2mp 22312. (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 22310* | Lemma 4 for mp2pm2mp 22312. (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 22311* | Lemma 5 for mp2pm2mp 22312. (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 22312* | 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 22313* | Lemma 2 for pm2mpghm 22317. (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 22314 | 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 22315 | 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 22316 | 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 22317 | 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 22318 | 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 22319* | Lemma 1 for pm2mpmhm 22321. (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 22320* | Lemma 2 for pm2mpmhm 22321. (Contributed by AV, 22-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = (Poly1โ๐ ) & โข ๐ถ = (๐ Mat ๐) & โข ๐ด = (๐ Mat ๐ ) & โข ๐ = (Poly1โ๐ด) & โข ๐ = (๐ pMatToMatPoly ๐ ) & โข ๐ต = (Baseโ๐ถ) โ โข ((๐ โ Fin โง ๐ โ Ring) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐โ(๐ฅ(.rโ๐ถ)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐)(๐โ๐ฆ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpmhm 22321 | 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 22322 | 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 22323 | 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 22324 | 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 22325 | 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 22326* | 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 22328) the eigenvalues and corresponding eigenvectors can be defined. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
The characteristic polynomial of a matrix ๐ด is the determinant of the characteristic matrix of ๐ด: (๐ก๐ผ โ ๐ด). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cchpmat 22327 | Extend class notation with the characteristic polynomial. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class CharPlyMat | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-chpmat 22328* | 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 22329 | 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 22330 | 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 22331* | 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 22332 | 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 22333 | 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 22334* | 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 22335 | The characteristic polynomial of the empty matrix. (Contributed by AV, 6-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ถ = (โ CharPlyMat ๐ ) โ โข (๐ โ Ring โ (๐ถโโ ) = (1rโ(Poly1โ๐ ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat1dlem 22336 | Lemma for chpmat1d 22337. (Contributed by AV, 7-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ถ = (๐ CharPlyMat ๐ ) & โข ๐ = (Poly1โ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (var1โ๐ ) & โข โ = (-gโ๐) & โข ๐ = (algScโ๐) & โข ๐บ = (๐ Mat ๐) & โข ๐ = (๐ matToPolyMat ๐ ) โ โข ((๐ โ Ring โง (๐ = {๐ผ} โง ๐ผ โ ๐) โง ๐ โ ๐ต) โ (๐ผ((๐( ยท๐ โ๐บ)(1rโ๐บ))(-gโ๐บ)(๐โ๐))๐ผ) = (๐ โ (๐โ(๐ผ๐๐ผ)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat1d 22337 | 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 22338 | Lemma 0 for chpdmat 22342. (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 22339 | Lemma 1 for chpdmat 22342. (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 22340 | Lemma 2 for chpdmat 22342. (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 22341 | Lemma 3 for chpdmat 22342. (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 22342* | 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 22343* | 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 22344* | 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 22345* | 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 22346* | 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 22347 | 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 22348 | 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 22349 | 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 22379. 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 22367, cayhamlem3 22388 and cayhamlem4 22389. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04if 22350* | 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 22351* | 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 22352* | 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 22353* | 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 22354* | 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 22355* | 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 22356* | 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 22357* | 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 22358* | 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 22359* | 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 22360* | 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 22361* | 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 22362* | 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 22363* | 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 22364* | 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 22365* | 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 22366* | 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 22367* | Lemma 1 for cayleyhamilton 22391. (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 22368 | The right-hand fundamental relation of the adjugate (see madurid 22145) 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 22369* | 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 22370* | 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 22371* | Lemma 1 for cpmidpmat 22374. (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 22372* | Lemma 2 for cpmidpmat 22374. (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 22373* | Lemma 3 for cpmidpmat 22374. (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 22374* | 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 22375* | Lemma B for cpmadugsum 22379. (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 22376* | Lemma C for cpmadugsum 22379. (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 22377* | Lemma F for cpmadugsum 22379. (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 22378* | 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 22379* | 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 โฆ ((๐ โ ๐) ยท (๐บโ๐))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidgsum2 22380* | Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as another group 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))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) & โข ๐ถ = (๐ CharPlyMat ๐ ) & โข ๐พ = (๐ถโ๐) & โข ๐ป = (๐พ ยท 1 ) โ โข ((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))๐ป = (๐ ฮฃg (๐ โ โ0 โฆ ((๐ โ ๐) ยท (๐บโ๐))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidg2sum 22381* | Equality of two sums representing the identity matrix multiplied with the characteristic polynomial of a matrix. (Contributed by AV, 11-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))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) & โข ๐ถ = (๐ CharPlyMat ๐ ) & โข ๐พ = (๐ถโ๐) & โข ๐ = (algScโ๐) โ โข ((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ ฮฃg (๐ โ โ0 โฆ ((๐ โ ๐) ยท ((๐โ((coe1โ๐พ)โ๐)) ยท 1 )))) = (๐ ฮฃg (๐ โ โ0 โฆ ((๐ โ ๐) ยท (๐บโ๐))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadumatpolylem1 22382* | Lemma 1 for cpmadumatpoly 22384. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (Poly1โ๐ ) & โข ๐ = (๐ Mat ๐) & โข ๐ = (๐ matToPolyMat ๐ ) & โข ร = (.rโ๐) & โข โ = (-gโ๐) & โข 0 = (0gโ๐) & โข ๐บ = (๐ โ โ0 โฆ if(๐ = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) & โข ๐ = (๐ ConstPolyMat ๐ ) & โข ยท = ( ยท๐ โ๐) & โข 1 = (1rโ๐) & โข ๐ = (var1โ๐ ) & โข ๐ท = ((๐ ยท 1 ) โ (๐โ๐)) & โข ๐ฝ = (๐ maAdju ๐) & โข ๐ = (Baseโ๐) & โข ๐ = (Poly1โ๐ด) & โข ๐ = (var1โ๐ด) & โข โ = ( ยท๐ โ๐) & โข โ = (.gโ(mulGrpโ๐)) & โข ๐ = (๐ cPolyMatToMat ๐ ) โ โข ((((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ โ ๐บ) โ (๐ต โm โ0)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadumatpolylem2 22383* | Lemma 2 for cpmadumatpoly 22384. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (Poly1โ๐ ) & โข ๐ = (๐ Mat ๐) & โข ๐ = (๐ matToPolyMat ๐ ) & โข ร = (.rโ๐) & โข โ = (-gโ๐) & โข 0 = (0gโ๐) & โข ๐บ = (๐ โ โ0 โฆ if(๐ = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) & โข ๐ = (๐ ConstPolyMat ๐ ) & โข ยท = ( ยท๐ โ๐) & โข 1 = (1rโ๐) & โข ๐ = (var1โ๐ ) & โข ๐ท = ((๐ ยท 1 ) โ (๐โ๐)) & โข ๐ฝ = (๐ maAdju ๐) & โข ๐ = (Baseโ๐) & โข ๐ = (Poly1โ๐ด) & โข ๐ = (var1โ๐ด) & โข โ = ( ยท๐ โ๐) & โข โ = (.gโ(mulGrpโ๐)) & โข ๐ = (๐ cPolyMatToMat ๐ ) โ โข ((((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ โ ๐บ) finSupp (0gโ๐ด)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadumatpoly 22384* | The product of the characteristic matrix of a given matrix and its adjunct represented as a polynomial over matrices. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 7-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (Poly1โ๐ ) & โข ๐ = (๐ Mat ๐) & โข ๐ = (๐ matToPolyMat ๐ ) & โข ร = (.rโ๐) & โข โ = (-gโ๐) & โข 0 = (0gโ๐) & โข ๐บ = (๐ โ โ0 โฆ if(๐ = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) & โข ๐ = (๐ ConstPolyMat ๐ ) & โข ยท = ( ยท๐ โ๐) & โข 1 = (1rโ๐) & โข ๐ = (var1โ๐ ) & โข ๐ท = ((๐ ยท 1 ) โ (๐โ๐)) & โข ๐ฝ = (๐ maAdju ๐) & โข ๐ = (Baseโ๐) & โข ๐ = (Poly1โ๐ด) & โข ๐ = (var1โ๐ด) & โข โ = ( ยท๐ โ๐) & โข โ = (.gโ(mulGrpโ๐)) & โข ๐ = (๐ cPolyMatToMat ๐ ) & โข ๐ผ = (๐ pMatToMatPoly ๐ ) โ โข ((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ผโ(๐ท ร (๐ฝโ๐ท))) = (๐ ฮฃg (๐ โ โ0 โฆ ((๐โ(๐บโ๐)) โ (๐ โ ๐))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayhamlem2 22385 | Lemma for cayhamlem3 22388. (Contributed by AV, 24-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐พ = (Baseโ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข โ = (.gโ(mulGrpโ๐ด)) & โข ยท = (.rโ๐ด) โ โข (((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โง (๐ป โ (๐พ โm โ0) โง ๐ฟ โ โ0)) โ ((๐ปโ๐ฟ) โ (๐ฟ โ ๐)) = ((๐ฟ โ ๐) ยท ((๐ปโ๐ฟ) โ 1 ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chcoeffeqlem 22386* | Lemma for chcoeffeq 22387. (Contributed by AV, 21-Nov-2019.) (Proof shortened by AV, 7-Dec-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (Poly1โ๐ ) & โข ๐ = (๐ Mat ๐) & โข ร = (.rโ๐) & โข โ = (-gโ๐) & โข 0 = (0gโ๐) & โข ๐ = (๐ matToPolyMat ๐ ) & โข ๐ถ = (๐ CharPlyMat ๐ ) & โข ๐พ = (๐ถโ๐) & โข ๐บ = (๐ โ โ0 โฆ if(๐ = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) & โข ๐ = (Baseโ๐) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข ๐ = (๐ cPolyMatToMat ๐ ) โ โข (((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ (((Poly1โ๐ด) ฮฃg (๐ โ โ0 โฆ ((๐โ(๐บโ๐))( ยท๐ โ(Poly1โ๐ด))(๐(.gโ(mulGrpโ(Poly1โ๐ด)))(var1โ๐ด))))) = ((Poly1โ๐ด) ฮฃg (๐ โ โ0 โฆ ((((coe1โ๐พ)โ๐) โ 1 )( ยท๐ โ(Poly1โ๐ด))(๐(.gโ(mulGrpโ(Poly1โ๐ด)))(var1โ๐ด))))) โ โ๐ โ โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chcoeffeq 22387* | The coefficients of the characteristic polynomial multiplied with the identity matrix represented by (transformed) ring elements obtained from the adjunct of the characteristic matrix. (Contributed by AV, 21-Nov-2019.) (Proof shortened by AV, 8-Dec-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (Poly1โ๐ ) & โข ๐ = (๐ Mat ๐) & โข ร = (.rโ๐) & โข โ = (-gโ๐) & โข 0 = (0gโ๐) & โข ๐ = (๐ matToPolyMat ๐ ) & โข ๐ถ = (๐ CharPlyMat ๐ ) & โข ๐พ = (๐ถโ๐) & โข ๐บ = (๐ โ โ0 โฆ if(๐ = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) & โข ๐ = (Baseโ๐) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข ๐ = (๐ cPolyMatToMat ๐ ) โ โข ((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))โ๐ โ โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 )) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayhamlem3 22388* | Lemma for cayhamlem4 22389. (Contributed by AV, 24-Nov-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (Poly1โ๐ ) & โข ๐ = (๐ Mat ๐) & โข ร = (.rโ๐) & โข โ = (-gโ๐) & โข 0 = (0gโ๐) & โข ๐ = (๐ matToPolyMat ๐ ) & โข ๐ถ = (๐ CharPlyMat ๐ ) & โข ๐พ = (๐ถโ๐) & โข ๐บ = (๐ โ โ0 โฆ if(๐ = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) & โข ๐ = (Baseโ๐) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข ๐ = (๐ cPolyMatToMat ๐ ) & โข โ = (.gโ(mulGrpโ๐ด)) & โข ยท = (.rโ๐ด) โ โข ((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ด ฮฃg (๐ โ โ0 โฆ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)))) = (๐ด ฮฃg (๐ โ โ0 โฆ ((๐ โ ๐) ยท (๐โ(๐บโ๐)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayhamlem4 22389* | Lemma for cayleyhamilton 22391. (Contributed by AV, 25-Nov-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (Poly1โ๐ ) & โข ๐ = (๐ Mat ๐) & โข ร = (.rโ๐) & โข โ = (-gโ๐) & โข 0 = (0gโ๐) & โข ๐ = (๐ matToPolyMat ๐ ) & โข ๐ถ = (๐ CharPlyMat ๐ ) & โข ๐พ = (๐ถโ๐) & โข ๐บ = (๐ โ โ0 โฆ if(๐ = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) & โข ๐ = (Baseโ๐) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข ๐ = (๐ cPolyMatToMat ๐ ) & โข โ = (.gโ(mulGrpโ๐ด)) & โข ๐ธ = (.gโ(mulGrpโ๐)) โ โข ((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ด ฮฃg (๐ โ โ0 โฆ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)))) = (๐โ(๐ ฮฃg (๐ โ โ0 โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayleyhamilton0 22390* | The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation". This version of cayleyhamilton 22391 provides definitions not used in the theorem itself, but in its proof to make it clearer, more readable and shorter compared with a proof without them (see cayleyhamiltonALT 22392)! (Contributed by AV, 25-Nov-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข 0 = (0gโ๐ด) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข โ = (.gโ(mulGrpโ๐ด)) & โข ๐ถ = (๐ CharPlyMat ๐ ) & โข ๐พ = (coe1โ(๐ถโ๐)) & โข ๐ = (Poly1โ๐ ) & โข ๐ = (๐ Mat ๐) & โข ร = (.rโ๐) & โข โ = (-gโ๐) & โข ๐ = (0gโ๐) & โข ๐ = (Baseโ๐) & โข ๐ธ = (.gโ(mulGrpโ๐)) & โข ๐ = (๐ matToPolyMat ๐ ) & โข ๐บ = (๐ โ โ0 โฆ if(๐ = 0, (๐ โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, ๐, ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) & โข ๐ = (๐ cPolyMatToMat ๐ ) โ โข ((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โ (๐ด ฮฃg (๐ โ โ0 โฆ ((๐พโ๐) โ (๐ โ ๐)))) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayleyhamilton 22391* | The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation", see theorem 7.8 in [Roman] p. 170 (without proof!), or theorem 3.1 in [Lang] p. 561. In other words, a matrix over a commutative ring "inserted" into its characteristic polynomial results in zero. This is Metamath 100 proof #49. (Contributed by Alexander van der Vekens, 25-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข 0 = (0gโ๐ด) & โข ๐ถ = (๐ CharPlyMat ๐ ) & โข ๐พ = (coe1โ(๐ถโ๐)) & โข โ = ( ยท๐ โ๐ด) & โข โ = (.gโ(mulGrpโ๐ด)) โ โข ((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โ (๐ด ฮฃg (๐ โ โ0 โฆ ((๐พโ๐) โ (๐ โ ๐)))) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayleyhamiltonALT 22392* | Alternate proof of cayleyhamilton 22391, the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 22390 directly, but has the same structure as the proof of cayleyhamilton0 22390. In contrast to the proof of cayleyhamilton0 22390, only the definitions required to formulate the theorem itself are used, causing the definitions used in the lemmas being expanded, which makes the proof longer and more difficult to read. (Contributed by AV, 25-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข 0 = (0gโ๐ด) & โข ๐ถ = (๐ CharPlyMat ๐ ) & โข ๐พ = (coe1โ(๐ถโ๐)) & โข โ = ( ยท๐ โ๐ด) & โข โ = (.gโ(mulGrpโ๐ด)) โ โข ((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โ (๐ด ฮฃg (๐ โ โ0 โฆ ((๐พโ๐) โ (๐ โ ๐)))) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayleyhamilton1 22393* | The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation", or, in other words, a matrix over a commutative ring "inserted" into its characteristic polynomial results in zero. In this variant of cayleyhamilton 22391, the meaning of "inserted" is made more transparent: If the characteristic polynomial is a polynomial with coefficients (๐นโ๐), then a matrix over a commutative ring "inserted" into its characteristic polynomial is the sum of these coefficients multiplied with the corresponding power of the matrix. (Contributed by AV, 25-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข 0 = (0gโ๐ด) & โข ๐ถ = (๐ CharPlyMat ๐ ) & โข ๐พ = (coe1โ(๐ถโ๐)) & โข โ = ( ยท๐ โ๐ด) & โข โ = (.gโ(mulGrpโ๐ด)) & โข ๐ฟ = (Baseโ๐ ) & โข ๐ = (var1โ๐ ) & โข ๐ = (Poly1โ๐ ) & โข ยท = ( ยท๐ โ๐) & โข ๐ธ = (.gโ(mulGrpโ๐)) & โข ๐ = (0gโ๐ ) โ โข (((๐ โ Fin โง ๐ โ CRing โง ๐ โ ๐ต) โง (๐น โ (๐ฟ โm โ0) โง ๐น finSupp ๐)) โ ((๐ถโ๐) = (๐ ฮฃg (๐ โ โ0 โฆ ((๐นโ๐) ยท (๐๐ธ๐)))) โ (๐ด ฮฃg (๐ โ โ0 โฆ ((๐นโ๐) โ (๐ โ ๐)))) = 0 )) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
A topology on a set is a set of subsets of that set, called open sets, which satisfy certain conditions. One condition is that the whole set be an open set. Therefore, a set is recoverable from a topology on it (as its union, see toponuni 22415), and it may sometimes be more convenient to consider topologies without reference to the underlying set. This is why we define successively the class of topologies (df-top 22395), then the function which associates with a set the set of topologies on it (df-topon 22412), and finally the class of topological spaces, as extensible structures having an underlying set and a topology on it (df-topsp 22434). Of course, a topology is the same thing as a topology on a set (see toprntopon 22426). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ctop 22394 | Syntax for the class of topologies. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class Top | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-top 22395* |
Define the class of topologies. It is a proper class (see topnex 22498).
See istopg 22396 and istop2g 22397 for the corresponding characterizations,
using respectively binary intersections like in this definition and
nonempty finite intersections.
The final form of the definition is due to Bourbaki (Def. 1 of [BourbakiTop1] p. I.1), while the idea of defining a topology in terms of its open sets is due to Aleksandrov. For the convoluted history of the definitions of these notions, see Gregory H. Moore, The emergence of open sets, closed sets, and limit points in analysis and topology, Historia Mathematica 35 (2008) 220--241. (Contributed by NM, 3-Mar-2006.) (Revised by BJ, 20-Oct-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข Top = {๐ฅ โฃ (โ๐ฆ โ ๐ซ ๐ฅโช ๐ฆ โ ๐ฅ โง โ๐ฆ โ ๐ฅ โ๐ง โ ๐ฅ (๐ฆ โฉ ๐ง) โ ๐ฅ)} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | istopg 22396* |
Express the predicate "๐ฝ is a topology". See istop2g 22397 for another
characterization using nonempty finite intersections instead of binary
intersections.
Note: In the literature, a topology is often represented by a calligraphic letter T, which resembles the letter J. This confusion may have led to J being used by some authors (e.g., K. D. Joshi, Introduction to General Topology (1983), p. 114) and it is convenient for us since we later use ๐ to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ฝ โ ๐ด โ (๐ฝ โ Top โ (โ๐ฅ(๐ฅ โ ๐ฝ โ โช ๐ฅ โ ๐ฝ) โง โ๐ฅ โ ๐ฝ โ๐ฆ โ ๐ฝ (๐ฅ โฉ ๐ฆ) โ ๐ฝ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | istop2g 22397* | Express the predicate "๐ฝ is a topology" using nonempty finite intersections instead of binary intersections as in istopg 22396. (Contributed by NM, 19-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ฝ โ ๐ด โ (๐ฝ โ Top โ (โ๐ฅ(๐ฅ โ ๐ฝ โ โช ๐ฅ โ ๐ฝ) โง โ๐ฅ((๐ฅ โ ๐ฝ โง ๐ฅ โ โ โง ๐ฅ โ Fin) โ โฉ ๐ฅ โ ๐ฝ)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uniopn 22398 | The union of a subset of a topology (that is, the union of any family of open sets of a topology) is an open set. (Contributed by Stefan Allan, 27-Feb-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ฝ โ Top โง ๐ด โ ๐ฝ) โ โช ๐ด โ ๐ฝ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iunopn 22399* | The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ฝ โ Top โง โ๐ฅ โ ๐ด ๐ต โ ๐ฝ) โ โช ๐ฅ โ ๐ด ๐ต โ ๐ฝ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | inopn 22400 | The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ฝ โ Top โง ๐ด โ ๐ฝ โง ๐ต โ ๐ฝ) โ (๐ด โฉ ๐ต) โ ๐ฝ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |