Home | Metamath
Proof Explorer Theorem List (p. 222 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chmatval 22101 | 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 22102* | 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 22103 | 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 22104 | 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 22105* | 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 22106 | The characteristic polynomial of the empty matrix. (Contributed by AV, 6-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (β CharPlyMat π ) β β’ (π β Ring β (πΆββ ) = (1rβ(Poly1βπ ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat1dlem 22107 | Lemma for chpmat1d 22108. (Contributed by AV, 7-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π CharPlyMat π ) & β’ π = (Poly1βπ ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (var1βπ ) & β’ β = (-gβπ) & β’ π = (algScβπ) & β’ πΊ = (π Mat π) & β’ π = (π matToPolyMat π ) β β’ ((π β Ring β§ (π = {πΌ} β§ πΌ β π) β§ π β π΅) β (πΌ((π( Β·π βπΊ)(1rβπΊ))(-gβπΊ)(πβπ))πΌ) = (π β (πβ(πΌππΌ)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat1d 22108 | 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 22109 | Lemma 0 for chpdmat 22113. (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 22110 | Lemma 1 for chpdmat 22113. (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 22111 | Lemma 2 for chpdmat 22113. (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 22112 | Lemma 3 for chpdmat 22113. (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 22113* | 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 22114* | 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 22115* | 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 22116* | 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 22117* | 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 22118 | 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 22119 | 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 22120 | 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 22150. 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 22138, cayhamlem3 22159 and cayhamlem4 22160. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04if 22121* | 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 22122* | 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 22123* | 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 22124* | 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 22125* | 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 22126* | 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 22127* | 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 22128* | 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 22129* | 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 22130* | 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 22131* | 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 22132* | 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 22133* | 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 22134* | 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 22135* | 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 22136* | 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 22137* | 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 22138* | Lemma 1 for cayleyhamilton 22162. (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 22139 | The right-hand fundamental relation of the adjugate (see madurid 21916) 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 22140* | 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 22141* | 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 22142* | Lemma 1 for cpmidpmat 22145. (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 22143* | Lemma 2 for cpmidpmat 22145. (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 22144* | Lemma 3 for cpmidpmat 22145. (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 22145* | 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 22146* | Lemma B for cpmadugsum 22150. (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 22147* | Lemma C for cpmadugsum 22150. (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 22148* | Lemma F for cpmadugsum 22150. (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 22149* | 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 22150* | 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 22151* | 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 22152* | 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 22153* | Lemma 1 for cpmadumatpoly 22155. (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 22154* | Lemma 2 for cpmadumatpoly 22155. (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 22155* | 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 22156 | Lemma for cayhamlem3 22159. (Contributed by AV, 24-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΎ = (Baseβπ ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ 1 = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ β = (.gβ(mulGrpβπ΄)) & β’ Β· = (.rβπ΄) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π» β (πΎ βm β0) β§ πΏ β β0)) β ((π»βπΏ) β (πΏ β π)) = ((πΏ β π) Β· ((π»βπΏ) β 1 ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chcoeffeqlem 22157* | Lemma for chcoeffeq 22158. (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 22158* | 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 22159* | Lemma for cayhamlem4 22160. (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 22160* | Lemma for cayleyhamilton 22162. (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 22161* | The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation". This version of cayleyhamilton 22162 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 22163)! (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 22162* | 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 22163* | Alternate proof of cayleyhamilton 22162, the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 22161 directly, but has the same structure as the proof of cayleyhamilton0 22161. In contrast to the proof of cayleyhamilton0 22161, 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 22164* | 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 22162, 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 22186), 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 22166), then the function which associates with a set the set of topologies on it (df-topon 22183), and finally the class of topological spaces, as extensible structures having an underlying set and a topology on it (df-topsp 22205). Of course, a topology is the same thing as a topology on a set (see toprntopon 22197). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ctop 22165 | Syntax for the class of topologies. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class Top | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-top 22166* |
Define the class of topologies. It is a proper class (see topnex 22269).
See istopg 22167 and istop2g 22168 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 22167* |
Express the predicate "π½ is a topology". See istop2g 22168 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 22168* | Express the predicate "π½ is a topology" using nonempty finite intersections instead of binary intersections as in istopg 22167. (Contributed by NM, 19-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π½ β π΄ β (π½ β Top β (βπ₯(π₯ β π½ β βͺ π₯ β π½) β§ βπ₯((π₯ β π½ β§ π₯ β β β§ π₯ β Fin) β β© π₯ β π½)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uniopn 22169 | 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 22170* | The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π½ β Top β§ βπ₯ β π΄ π΅ β π½) β βͺ π₯ β π΄ π΅ β π½) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | inopn 22171 | The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π½ β Top β§ π΄ β π½ β§ π΅ β π½) β (π΄ β© π΅) β π½) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fitop 22172 | A topology is closed under finite intersections. (Contributed by Jeff Hankins, 7-Oct-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π½ β Top β (fiβπ½) = π½) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fiinopn 22173 | The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π½ β Top β ((π΄ β π½ β§ π΄ β β β§ π΄ β Fin) β β© π΄ β π½)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iinopn 22174* | The intersection of a nonempty finite family of open sets is open. (Contributed by Mario Carneiro, 14-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π½ β Top β§ (π΄ β Fin β§ π΄ β β β§ βπ₯ β π΄ π΅ β π½)) β β© π₯ β π΄ π΅ β π½) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | unopn 22175 | The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π½ β Top β§ π΄ β π½ β§ π΅ β π½) β (π΄ βͺ π΅) β π½) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 0opn 22176 | The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π½ β Top β β β π½) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 0ntop 22177 | The empty set is not a topology. (Contributed by FL, 1-Jun-2008.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ Β¬ β β Top | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topopn 22178 | The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = βͺ π½ β β’ (π½ β Top β π β π½) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eltopss 22179 | A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π½) β π΄ β π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | riinopn 22180* | A finite indexed relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β Fin β§ βπ₯ β π΄ π΅ β π½) β (π β© β© π₯ β π΄ π΅) β π½) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | rintopn 22181 | A finite relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π½ β§ π΄ β Fin) β (π β© β© π΄) β π½) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ctopon 22182 | Syntax for the function of topologies on sets. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class TopOn | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-topon 22183* | Define the function that associates with a set the set of topologies on it. (Contributed by Stefan O'Rear, 31-Jan-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ TopOn = (π β V β¦ {π β Top β£ π = βͺ π}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | istopon 22184 | Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π½ β (TopOnβπ΅) β (π½ β Top β§ π΅ = βͺ π½)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topontop 22185 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π½ β (TopOnβπ΅) β π½ β Top) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponuni 22186 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π½ β (TopOnβπ΅) β π΅ = βͺ π½) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topontopi 22187 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π½ β (TopOnβπ΅) β β’ π½ β Top | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponunii 22188 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π½ β (TopOnβπ΅) β β’ π΅ = βͺ π½ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toptopon 22189 | Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π = βͺ π½ β β’ (π½ β Top β π½ β (TopOnβπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toptopon2 22190 | A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π½ β Top β π½ β (TopOnββͺ π½)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topontopon 22191 | A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π½ β (TopOnβπ) β π½ β (TopOnββͺ π½)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funtopon 22192 | The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ Fun TopOn | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponrestid 22193 | Given a topology on a set, restricting it to that same set has no effect. (Contributed by Jim Kingdon, 6-Jul-2022.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ β (TopOnβπ΅) β β’ π΄ = (π΄ βΎt π΅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponsspwpw 22194 | The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (TopOnβπ΄) β π« π« π΄ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | dmtopon 22195 | The domain of TopOn is the universal class V. (Contributed by BJ, 29-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ dom TopOn = V | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fntopon 22196 | The class TopOn is a function with domain the universal class V. Analogue for topologies of fnmre 17406 for Moore collections. (Contributed by BJ, 29-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ TopOn Fn V | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toprntopon 22197 | A topology is the same thing as a topology on a set (variable-free version). (Contributed by BJ, 27-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ Top = βͺ ran TopOn | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponmax 22198 | The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π½ β (TopOnβπ΅) β π΅ β π½) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponss 22199 | A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π½ β (TopOnβπ) β§ π΄ β π½) β π΄ β π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponcom 22200 | If πΎ is a topology on the base set of topology π½, then π½ is a topology on the base of πΎ. (Contributed by Mario Carneiro, 22-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π½ β Top β§ πΎ β (TopOnββͺ π½)) β π½ β (TopOnββͺ πΎ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |