Home | Metamath
Proof Explorer Theorem List (p. 322 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 | ||
Syntax | cextdg 32101 | Syntax for the field extension degree operation. |
class [:] | ||
Definition | df-fldext 32102* | Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ /FldExt = {β¨π, πβ© β£ ((π β Field β§ π β Field) β§ (π = (π βΎs (Baseβπ)) β§ (Baseβπ) β (SubRingβπ)))} | ||
Definition | df-extdg 32103* | Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ [:] = (π β V, π β (/FldExt β {π}) β¦ (dimβ((subringAlg βπ)β(Baseβπ)))) | ||
Definition | df-finext 32104* | Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ /FinExt = {β¨π, πβ© β£ (π/FldExtπ β§ (π[:]π) β β0)} | ||
Definition | df-algext 32105* | Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ /AlgExt = {β¨π, πβ© β£ (π/FldExtπ β§ βπ₯ β (Baseβπ)βπ β (Poly1βπ)(((eval1βπ)βπ)βπ₯) = (0gβπ))} | ||
Theorem | relfldext 32106 | The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ Rel /FldExt | ||
Theorem | brfldext 32107 | The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ ((πΈ β Field β§ πΉ β Field) β (πΈ/FldExtπΉ β (πΉ = (πΈ βΎs (BaseβπΉ)) β§ (BaseβπΉ) β (SubRingβπΈ)))) | ||
Theorem | ccfldextrr 32108 | The field of the complex numbers is an extension of the field of the real numbers. (Contributed by Thierry Arnoux, 20-Jul-2023.) |
β’ βfld/FldExtβfld | ||
Theorem | fldextfld1 32109 | A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β πΈ β Field) | ||
Theorem | fldextfld2 32110 | A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β πΉ β Field) | ||
Theorem | fldextsubrg 32111 | Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ π = (BaseβπΉ) β β’ (πΈ/FldExtπΉ β π β (SubRingβπΈ)) | ||
Theorem | fldextress 32112 | Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β πΉ = (πΈ βΎs (BaseβπΉ))) | ||
Theorem | brfinext 32113 | The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β (πΈ/FinExtπΉ β (πΈ[:]πΉ) β β0)) | ||
Theorem | extdgval 32114 | Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β (πΈ[:]πΉ) = (dimβ((subringAlg βπΈ)β(BaseβπΉ)))) | ||
Theorem | fldextsralvec 32115 | The subring algebra associated with a field extension is a vector space. (Contributed by Thierry Arnoux, 3-Aug-2023.) |
β’ (πΈ/FldExtπΉ β ((subringAlg βπΈ)β(BaseβπΉ)) β LVec) | ||
Theorem | extdgcl 32116 | Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β (πΈ[:]πΉ) β β0*) | ||
Theorem | extdggt0 32117 | Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ (πΈ/FldExtπΉ β 0 < (πΈ[:]πΉ)) | ||
Theorem | fldexttr 32118 | Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ ((πΈ/FldExtπΉ β§ πΉ/FldExtπΎ) β πΈ/FldExtπΎ) | ||
Theorem | fldextid 32119 | The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ (πΉ β Field β πΉ/FldExtπΉ) | ||
Theorem | extdgid 32120 | A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.) |
β’ (πΈ β Field β (πΈ[:]πΈ) = 1) | ||
Theorem | extdgmul 32121 | The multiplicativity formula for degrees of field extensions. Given πΈ a field extension of πΉ, itself a field extension of πΎ, the degree of the extension πΈ/FldExtπΎ is the product of the degrees of the extensions πΈ/FldExtπΉ and πΉ/FldExtπΎ. Proposition 1.2 of [Lang], p. 224. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ ((πΈ/FldExtπΉ β§ πΉ/FldExtπΎ) β (πΈ[:]πΎ) = ((πΈ[:]πΉ) Β·e (πΉ[:]πΎ))) | ||
Theorem | finexttrb 32122 | The extension πΈ of πΎ is finite if and only if πΈ is finite over πΉ and πΉ is finite over πΎ. Corollary 1.3 of [Lang] , p. 225. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ ((πΈ/FldExtπΉ β§ πΉ/FldExtπΎ) β (πΈ/FinExtπΎ β (πΈ/FinExtπΉ β§ πΉ/FinExtπΎ))) | ||
Theorem | extdg1id 32123 | If the degree of the extension πΈ/FldExtπΉ is 1, then πΈ and πΉ are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
β’ ((πΈ/FldExtπΉ β§ (πΈ[:]πΉ) = 1) β πΈ = πΉ) | ||
Theorem | extdg1b 32124 | The degree of the extension πΈ/FldExtπΉ is 1 iff πΈ and πΉ are the same structure. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
β’ (πΈ/FldExtπΉ β ((πΈ[:]πΉ) = 1 β πΈ = πΉ)) | ||
Theorem | fldextchr 32125 | The characteristic of a subfield is the same as the characteristic of the larger field. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ (πΈ/FldExtπΉ β (chrβπΉ) = (chrβπΈ)) | ||
Theorem | ccfldsrarelvec 32126 | The subring algebra of the complex numbers over the real numbers is a left vector space. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ ((subringAlg ββfld)ββ) β LVec | ||
Theorem | ccfldextdgrr 32127 | The degree of the field extension of the complex numbers over the real numbers is 2. (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ (βfld[:]βfld) = 2 | ||
Syntax | calgnb 32128 | Extend class notation with the algebraic number builder function. |
class AlgNb | ||
Syntax | cminply 32129 | Extend class notation with the minimal polynomial builder function. |
class minPoly | ||
Definition | df-algnb 32130* | Define the algebraic number builder function. This definition is similar to df-aa 25597. (Contributed by Thierry Arnoux, 19-Jan-2025.) |
β’ AlgNb = (π β V, π β V β¦ βͺ π β (dom (π evalSub1 π) β {(0gβ(Poly1βπ))})(β‘((π evalSub1 π)βπ) β {(0gβπ)})) | ||
Definition | df-minply 32131* | Define the minimal polynomial builder function . (Contributed by Thierry Arnoux, 19-Jan-2025.) |
β’ minPoly = (π β V, π β V β¦ (π₯ β (π AlgNb π) β¦ inf((β‘((π evalSub1 π)βπ) β {(0gβπ)}), (Monic1pβπ), (( deg1 βπ) βr < ( deg1 βπ))))) | ||
Theorem | algnbval 32132* | The algebraic numbers over a field πΉ within a field πΈ. That is, the numbers π which are roots of nonzero polynomials π(π) with coefficients in (BaseβπΉ). This is expressed by the idiom (β‘(πβπ) β { 0 }), which can be translated into {π₯ β (BaseβπΈ) β£ ((πβπ)βπ₯) = 0 } by fniniseg2 7008. (Contributed by Thierry Arnoux, 26-Jan-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (0gβ(Poly1βπΈ)) & β’ 0 = (0gβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) β β’ (π β (πΈ AlgNb πΉ) = βͺ π β (dom π β {π})(β‘(πβπ) β { 0 })) | ||
Theorem | isalgnb 32133* | Property for an element π of a field πΈ to be algebraic over a subfield πΉ. (Contributed by Thierry Arnoux, 26-Jan-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (0gβ(Poly1βπΈ)) & β’ 0 = (0gβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ π΅ = (BaseβπΈ) β β’ (π β (π β (πΈ AlgNb πΉ) β (π β π΅ β§ βπ β (dom π β {π})((πβπ)βπ) = 0 ))) | ||
Theorem | minplyeulem 32134* | An algebraic number π over πΉ is a root of some monic polynomial π with coefficients in πΉ. (Contributed by Thierry Arnoux, 26-Jan-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (0gβ(Poly1βπΈ)) & β’ 0 = (0gβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π β (πΈ AlgNb πΉ)) β β’ (π β βπ β (Monic1pβπΈ)((πβπ)βπ) = 0 ) | ||
Syntax | csmat 32135 | Syntax for a function generating submatrices. |
class subMat1 | ||
Definition | df-smat 32136* | Define a function generating submatrices of an integer-indexed matrix. The function maps an index in ((1...π) Γ (1...π)) into a new index in ((1...(π β 1)) Γ (1...(π β 1))). A submatrix is obtained by deleting a row and a column of the original matrix. Because this function re-indexes the matrix, the resulting submatrix still has the same index set for rows and columns, and its determinent is defined, unlike the current df-subma 21848. (Contributed by Thierry Arnoux, 18-Aug-2020.) |
β’ subMat1 = (π β V β¦ (π β β, π β β β¦ (π β (π β β, π β β β¦ β¨if(π < π, π, (π + 1)), if(π < π, π, (π + 1))β©)))) | ||
Theorem | smatfval 32137* | Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ ((πΎ β β β§ πΏ β β β§ π β π) β (πΎ(subMat1βπ)πΏ) = (π β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) | ||
Theorem | smatrcl 32138 | Closure of the rectangular submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) β β’ (π β π β (π΅ βm ((1...(π β 1)) Γ (1...(π β 1))))) | ||
Theorem | smatlem 32139 | Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β β) & β’ (π β π½ β β) & β’ (π β if(πΌ < πΎ, πΌ, (πΌ + 1)) = π) & β’ (π β if(π½ < πΏ, π½, (π½ + 1)) = π) β β’ (π β (πΌππ½) = (ππ΄π)) | ||
Theorem | smattl 32140 | Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β (1..^πΎ)) & β’ (π β π½ β (1..^πΏ)) β β’ (π β (πΌππ½) = (πΌπ΄π½)) | ||
Theorem | smattr 32141 | Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β (πΎ...π)) & β’ (π β π½ β (1..^πΏ)) β β’ (π β (πΌππ½) = ((πΌ + 1)π΄π½)) | ||
Theorem | smatbl 32142 | Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β (1..^πΎ)) & β’ (π β π½ β (πΏ...π)) β β’ (π β (πΌππ½) = (πΌπ΄(π½ + 1))) | ||
Theorem | smatbr 32143 | Entries of a submatrix, bottom right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β (πΎ...π)) & β’ (π β π½ β (πΏ...π)) β β’ (π β (πΌππ½) = ((πΌ + 1)π΄(π½ + 1))) | ||
Theorem | smatcl 32144 | Closure of the square submatrix: if π is a square matrix of dimension π with indices in (1...π), then a submatrix of π is of dimension (π β 1). (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π΄ = ((1...π) Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΆ = (Baseβ((1...(π β 1)) Mat π )) & β’ π = (πΎ(subMat1βπ)πΏ) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π β π΅) β β’ (π β π β πΆ) | ||
Theorem | matmpo 32145* | Write a square matrix as a mapping operation. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) β β’ (π β π΅ β π = (π β π, π β π β¦ (πππ))) | ||
Theorem | 1smat1 32146 | The submatrix of the identity matrix obtained by removing the ith row and the ith column is an identity matrix. Cf. 1marepvsma1 21854. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ 1 = (1rβ((1...π) Mat π )) & β’ (π β π β Ring) & β’ (π β π β β) & β’ (π β πΌ β (1...π)) β β’ (π β (πΌ(subMat1β 1 )πΌ) = (1rβ((1...(π β 1)) Mat π ))) | ||
Theorem | submat1n 32147 | One case where the submatrix with integer indices, subMat1, and the general submatrix subMat, agree. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΄ = ((1...π) Mat π ) & β’ π΅ = (Baseβπ΄) β β’ ((π β β β§ π β π΅) β (π(subMat1βπ)π) = (π(((1...π) subMat π )βπ)π)) | ||
Theorem | submatres 32148 | Special case where the submatrix is a restriction of the initial matrix, and no renumbering occurs. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
β’ π΄ = ((1...π) Mat π ) & β’ π΅ = (Baseβπ΄) β β’ ((π β β β§ π β π΅) β (π(subMat1βπ)π) = (π βΎ ((1...(π β 1)) Γ (1...(π β 1))))) | ||
Theorem | submateqlem1 32149 | Lemma for submateq 32151. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β π β (1...(π β 1))) & β’ (π β πΎ β€ π) β β’ (π β (π β (πΎ...π) β§ (π + 1) β ((1...π) β {πΎ}))) | ||
Theorem | submateqlem2 32150 | Lemma for submateq 32151. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β π β (1...(π β 1))) & β’ (π β π < πΎ) β β’ (π β (π β (1..^πΎ) β§ π β ((1...π) β {πΎ}))) | ||
Theorem | submateq 32151* | Sufficient condition for two submatrices to be equal. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
β’ π΄ = ((1...π) Mat π ) & β’ π΅ = (Baseβπ΄) & β’ (π β π β β) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) & β’ ((π β§ π β ((1...π) β {πΌ}) β§ π β ((1...π) β {π½})) β (ππΈπ) = (ππΉπ)) β β’ (π β (πΌ(subMat1βπΈ)π½) = (πΌ(subMat1βπΉ)π½)) | ||
Theorem | submatminr1 32152 | If we take a submatrix by removing the row πΌ and column π½, then the result is the same on the matrix with row πΌ and column π½ modified by the minMatR1 operator. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
β’ π΄ = ((1...π) Mat π ) & β’ π΅ = (Baseβπ΄) & β’ (π β π β β) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ πΈ = (πΌ(((1...π) minMatR1 π )βπ)π½) β β’ (π β (πΌ(subMat1βπ)π½) = (πΌ(subMat1βπΈ)π½)) | ||
Syntax | clmat 32153 | Extend class notation with the literal matrix conversion function. |
class litMat | ||
Definition | df-lmat 32154* | Define a function converting words of words into matrices. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ litMat = (π β V β¦ (π β (1...(β―βπ)), π β (1...(β―β(πβ0))) β¦ ((πβ(π β 1))β(π β 1)))) | ||
Theorem | lmatval 32155* | Value of the literal matrix conversion function. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ (π β π β (litMatβπ) = (π β (1...(β―βπ)), π β (1...(β―β(πβ0))) β¦ ((πβ(π β 1))β(π β 1)))) | ||
Theorem | lmatfval 32156* | Entries of a literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ π = (litMatβπ) & β’ (π β π β β) & β’ (π β π β Word Word π) & β’ (π β (β―βπ) = π) & β’ ((π β§ π β (0..^π)) β (β―β(πβπ)) = π) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) β β’ (π β (πΌππ½) = ((πβ(πΌ β 1))β(π½ β 1))) | ||
Theorem | lmatfvlem 32157* | Useful lemma to extract literal matrix entries. Suggested by Mario Carneiro. (Contributed by Thierry Arnoux, 3-Sep-2020.) |
β’ π = (litMatβπ) & β’ (π β π β β) & β’ (π β π β Word Word π) & β’ (π β (β―βπ) = π) & β’ ((π β§ π β (0..^π)) β (β―β(πβπ)) = π) & β’ πΎ β β0 & β’ πΏ β β0 & β’ πΌ β€ π & β’ π½ β€ π & β’ (πΎ + 1) = πΌ & β’ (πΏ + 1) = π½ & β’ (πβπΎ) = π & β’ (π β (πβπΏ) = π) β β’ (π β (πΌππ½) = π) | ||
Theorem | lmatcl 32158* | Closure of the literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
β’ π = (litMatβπ) & β’ (π β π β β) & β’ (π β π β Word Word π) & β’ (π β (β―βπ) = π) & β’ ((π β§ π β (0..^π)) β (β―β(πβπ)) = π) & β’ π = (Baseβπ ) & β’ π = ((1...π) Mat π ) & β’ π = (Baseβπ) & β’ (π β π β π) β β’ (π β π β π) | ||
Theorem | lmat22lem 32159* | Lemma for lmat22e11 32160 and co. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ ((π β§ π β (0..^2)) β (β―β(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ)) = 2) | ||
Theorem | lmat22e11 32160 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (1π1) = π΄) | ||
Theorem | lmat22e12 32161 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (1π2) = π΅) | ||
Theorem | lmat22e21 32162 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (2π1) = πΆ) | ||
Theorem | lmat22e22 32163 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (2π2) = π·) | ||
Theorem | lmat22det 32164 | The determinant of a literal 2x2 complex matrix. (Contributed by Thierry Arnoux, 1-Sep-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ π = (Baseβπ ) & β’ π½ = ((1...2) maDet π ) & β’ (π β π β Ring) β β’ (π β (π½βπ) = ((π΄ Β· π·) β (πΆ Β· π΅))) | ||
Theorem | mdetpmtr1 32165* | The determinant of a matrix with permuted rows is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π· = (π maDet π ) & β’ πΊ = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (β€RHomβπ ) & β’ Β· = (.rβπ ) & β’ πΈ = (π β π, π β π β¦ ((πβπ)ππ)) β β’ (((π β CRing β§ π β Fin) β§ (π β π΅ β§ π β πΊ)) β (π·βπ) = (((π β π)βπ) Β· (π·βπΈ))) | ||
Theorem | mdetpmtr2 32166* | The determinant of a matrix with permuted columns is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π· = (π maDet π ) & β’ πΊ = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (β€RHomβπ ) & β’ Β· = (.rβπ ) & β’ πΈ = (π β π, π β π β¦ (ππ(πβπ))) β β’ (((π β CRing β§ π β Fin) β§ (π β π΅ β§ π β πΊ)) β (π·βπ) = (((π β π)βπ) Β· (π·βπΈ))) | ||
Theorem | mdetpmtr12 32167* | The determinant of a matrix with permuted rows and columns is the determinant of the original matrix multiplied by the product of the signs of the permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π· = (π maDet π ) & β’ πΊ = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (β€RHomβπ ) & β’ Β· = (.rβπ ) & β’ πΈ = (π β π, π β π β¦ ((πβπ)π(πβπ))) & β’ (π β π β CRing) & β’ (π β π β Fin) & β’ (π β π β π΅) & β’ (π β π β πΊ) & β’ (π β π β πΊ) β β’ (π β (π·βπ) = ((πβ((πβπ) Β· (πβπ))) Β· (π·βπΈ))) | ||
Theorem | mdetlap1 32168* | A Laplace expansion of the determinant of a matrix, using the adjunct (cofactor) matrix. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π· = (π maDet π ) & β’ πΎ = (π maAdju π ) & β’ Β· = (.rβπ ) β β’ ((π β CRing β§ π β π΅ β§ πΌ β π) β (π·βπ) = (π Ξ£g (π β π β¦ ((πΌππ) Β· (π(πΎβπ)πΌ))))) | ||
Theorem | madjusmdetlem1 32169* | Lemma for madjusmdet 32173. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) & β’ πΊ = (Baseβ(SymGrpβ(1...π))) & β’ π = (pmSgnβ(1...π)) & β’ π = (πΌ(((1...π) minMatR1 π )βπ)π½) & β’ π = (π β (1...π), π β (1...π) β¦ ((πβπ)π(πβπ))) & β’ (π β π β πΊ) & β’ (π β π β πΊ) & β’ (π β (πβπ) = πΌ) & β’ (π β (πβπ) = π½) & β’ (π β (πΌ(subMat1βπ)π½) = (π(subMat1βπ)π)) β β’ (π β (π½(πΎβπ)πΌ) = ((πβ((πβπ) Β· (πβπ))) Β· (πΈβ(πΌ(subMat1βπ)π½)))) | ||
Theorem | madjusmdetlem2 32170* | Lemma for madjusmdet 32173. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) & β’ π = (π β (1...π) β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) β β’ ((π β§ π β (1...(π β 1))) β if(π < πΌ, π, (π + 1)) = ((π β β‘π)βπ)) | ||
Theorem | madjusmdetlem3 32171* | Lemma for madjusmdet 32173. (Contributed by Thierry Arnoux, 27-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) & β’ π = (π β (1...π) β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π½, if(π β€ π½, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) & β’ π = (π β (1...π), π β (1...π) β¦ (((π β β‘π)βπ)π((π β β‘π)βπ))) & β’ (π β π β π΅) β β’ (π β (πΌ(subMat1βπ)π½) = (π(subMat1βπ)π)) | ||
Theorem | madjusmdetlem4 32172* | Lemma for madjusmdet 32173. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) & β’ π = (π β (1...π) β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π½, if(π β€ π½, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) β β’ (π β (π½(πΎβπ)πΌ) = ((πβ(-1β(πΌ + π½))) Β· (πΈβ(πΌ(subMat1βπ)π½)))) | ||
Theorem | madjusmdet 32173 | Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrices. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) β β’ (π β (π½(πΎβπ)πΌ) = ((πβ(-1β(πΌ + π½))) Β· (πΈβ(πΌ(subMat1βπ)π½)))) | ||
Theorem | mdetlap 32174* | Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) β β’ (π β (π·βπ) = (π Ξ£g (π β (1...π) β¦ ((πβ(-1β(πΌ + π))) Β· ((πΌππ) Β· (πΈβ(πΌ(subMat1βπ)π))))))) | ||
Theorem | ist0cld 32175* | The predicate "is a T0 space", using closed sets. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ (π β π΅ = βͺ π½) & β’ (π β π· = (Clsdβπ½)) β β’ (π β (π½ β Kol2 β (π½ β Top β§ βπ₯ β π΅ βπ¦ β π΅ (βπ β π· (π₯ β π β π¦ β π) β π₯ = π¦)))) | ||
Theorem | txomap 32176* | Given two open maps πΉ and πΊ, π» mapping pairs of sets, is also an open map for the product topology. (Contributed by Thierry Arnoux, 29-Dec-2019.) |
β’ (π β πΉ:πβΆπ) & β’ (π β πΊ:πβΆπ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β π β (TopOnβπ)) & β’ ((π β§ π₯ β π½) β (πΉ β π₯) β πΏ) & β’ ((π β§ π¦ β πΎ) β (πΊ β π¦) β π) & β’ (π β π΄ β (π½ Γt πΎ)) & β’ π» = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) β β’ (π β (π» β π΄) β (πΏ Γt π)) | ||
Theorem | qtopt1 32177* | If every equivalence class is closed, then the quotient space is T1 . (Contributed by Thierry Arnoux, 5-Jan-2020.) |
β’ π = βͺ π½ & β’ (π β π½ β Fre) & β’ (π β πΉ:πβontoβπ) & β’ ((π β§ π₯ β π) β (β‘πΉ β {π₯}) β (Clsdβπ½)) β β’ (π β (π½ qTop πΉ) β Fre) | ||
Theorem | qtophaus 32178* | If an open map's graph in the product space (π½ Γt π½) is closed, then its quotient topology is Hausdorff. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
β’ π = βͺ π½ & β’ βΌ = (β‘πΉ β πΉ) & β’ π» = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) & β’ (π β π½ β Haus) & β’ (π β πΉ:πβontoβπ) & β’ ((π β§ π₯ β π½) β (πΉ β π₯) β (π½ qTop πΉ)) & β’ (π β βΌ β (Clsdβ(π½ Γt π½))) β β’ (π β (π½ qTop πΉ) β Haus) | ||
Theorem | circtopn 32179* | The topology of the unit circle is generated by open intervals of the polar coordinate. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
β’ πΌ = (0[,](2 Β· Ο)) & β’ π½ = (topGenβran (,)) & β’ πΉ = (π₯ β β β¦ (expβ(i Β· π₯))) & β’ πΆ = (β‘abs β {1}) β β’ (π½ qTop πΉ) = (TopOpenβ(πΉ βs βfld)) | ||
Theorem | circcn 32180* | The function gluing the real line into the unit circle is continuous. (Contributed by Thierry Arnoux, 5-Jan-2020.) |
β’ πΌ = (0[,](2 Β· Ο)) & β’ π½ = (topGenβran (,)) & β’ πΉ = (π₯ β β β¦ (expβ(i Β· π₯))) & β’ πΆ = (β‘abs β {1}) β β’ πΉ β (π½ Cn (π½ qTop πΉ)) | ||
Theorem | reff 32181* | For any cover refinement, there exists a function associating with each set in the refinement a set in the original cover containing it. This is sometimes used as a definition of refinement. Note that this definition uses the axiom of choice through ac6sg 10358. (Contributed by Thierry Arnoux, 12-Jan-2020.) |
β’ (π΄ β π β (π΄Refπ΅ β (βͺ π΅ β βͺ π΄ β§ βπ(π:π΄βΆπ΅ β§ βπ£ β π΄ π£ β (πβπ£))))) | ||
Theorem | locfinreflem 32182* | A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function π from the original cover π, which is taken as the index set. The solution is constructed by building unions, so the same method can be used to prove a similar theorem about closed covers. (Contributed by Thierry Arnoux, 29-Jan-2020.) |
β’ π = βͺ π½ & β’ (π β π β π½) & β’ (π β π = βͺ π) & β’ (π β π β π½) & β’ (π β πRefπ) & β’ (π β π β (LocFinβπ½)) β β’ (π β βπ((Fun π β§ dom π β π β§ ran π β π½) β§ (ran πRefπ β§ ran π β (LocFinβπ½)))) | ||
Theorem | locfinref 32183* | A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function π from the original cover π, which is taken as the index set. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ π = βͺ π½ & β’ (π β π β π½) & β’ (π β π = βͺ π) & β’ (π β π β π½) & β’ (π β πRefπ) & β’ (π β π β (LocFinβπ½)) β β’ (π β βπ(π:πβΆπ½ β§ ran πRefπ β§ ran π β (LocFinβπ½))) | ||
Syntax | ccref 32184 | The "every open cover has an π΄ refinement" predicate. |
class CovHasRefπ΄ | ||
Definition | df-cref 32185* | Define a statement "every open cover has an π΄ refinement" , where π΄ is a property for refinements like "finite", "countable", "point finite" or "locally finite". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ CovHasRefπ΄ = {π β Top β£ βπ¦ β π« π(βͺ π = βͺ π¦ β βπ§ β (π« π β© π΄)π§Refπ¦)} | ||
Theorem | iscref 32186* | The property that every open cover has an π΄ refinement for the topological space π½. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ π = βͺ π½ β β’ (π½ β CovHasRefπ΄ β (π½ β Top β§ βπ¦ β π« π½(π = βͺ π¦ β βπ§ β (π« π½ β© π΄)π§Refπ¦))) | ||
Theorem | crefeq 32187 | Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π΄ = π΅ β CovHasRefπ΄ = CovHasRefπ΅) | ||
Theorem | creftop 32188 | A space where every open cover has an π΄ refinement is a topological space. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π½ β CovHasRefπ΄ β π½ β Top) | ||
Theorem | crefi 32189* | The property that every open cover has an π΄ refinement for the topological space π½. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ π = βͺ π½ β β’ ((π½ β CovHasRefπ΄ β§ πΆ β π½ β§ π = βͺ πΆ) β βπ§ β (π« π½ β© π΄)π§RefπΆ) | ||
Theorem | crefdf 32190* | A formulation of crefi 32189 easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ π = βͺ π½ & β’ π΅ = CovHasRefπ΄ & β’ (π§ β π΄ β π) β β’ ((π½ β π΅ β§ πΆ β π½ β§ π = βͺ πΆ) β βπ§ β π« π½(π β§ π§RefπΆ)) | ||
Theorem | crefss 32191 | The "every open cover has an π΄ refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π΄ β π΅ β CovHasRefπ΄ β CovHasRefπ΅) | ||
Theorem | cmpcref 32192 | Equivalent definition of compact space in terms of open cover refinements. Compact spaces are topologies with finite open cover refinements. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ Comp = CovHasRefFin | ||
Theorem | cmpfiref 32193* | Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ π β π½ β§ π = βͺ π) β βπ£ β π« π½(π£ β Fin β§ π£Refπ)) | ||
Syntax | cldlf 32194 | Extend class notation with the class of all LindelΓΆf spaces. |
class Ldlf | ||
Definition | df-ldlf 32195 | Definition of a LindelΓΆf space. A LindelΓΆf space is a topological space in which every open cover has a countable subcover. Definition 1 of [BourbakiTop2] p. 195. (Contributed by Thierry Arnoux, 30-Jan-2020.) |
β’ Ldlf = CovHasRef{π₯ β£ π₯ βΌ Ο} | ||
Theorem | ldlfcntref 32196* | Every open cover of a LindelΓΆf space has a countable refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
β’ π = βͺ π½ β β’ ((π½ β Ldlf β§ π β π½ β§ π = βͺ π) β βπ£ β π« π½(π£ βΌ Ο β§ π£Refπ)) | ||
Syntax | cpcmp 32197 | Extend class notation with the class of all paracompact topologies. |
class Paracomp | ||
Definition | df-pcmp 32198 | Definition of a paracompact topology. A topology is said to be paracompact iff every open cover has an open refinement that is locally finite. The definition 6 of [BourbakiTop1] p. I.69. also requires the topology to be Hausdorff, but this is dropped here. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ Paracomp = {π β£ π β CovHasRef(LocFinβπ)} | ||
Theorem | ispcmp 32199 | The predicate "is a paracompact topology". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π½ β Paracomp β π½ β CovHasRef(LocFinβπ½)) | ||
Theorem | cmppcmp 32200 | Every compact space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π½ β Comp β π½ β Paracomp) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |