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