![]() |
Metamath
Proof Explorer Theorem List (p. 334 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | irngnzply1 33301* | In the case of a field πΈ, the roots of nonzero polynomials π with coefficients in a subfield πΉ are exactly the integral elements over πΉ. Roots of nonzero polynomials are called algebraic numbers, so this shows that in the case of a field, elements integral over πΉ are exactly the algebraic numbers. In this formula, dom π represents the polynomials, and π the zero polynomial. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (0gβ(Poly1βπΈ)) & β’ 0 = (0gβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) β β’ (π β (πΈ IntgRing πΉ) = βͺ π β (dom π β {π})(β‘(πβπ) β { 0 })) | ||
Syntax | cminply 33302 | Extend class notation with the minimal polynomial builder function. |
class minPoly | ||
Definition | df-minply 33303* | Define the minimal polynomial builder function. (Contributed by Thierry Arnoux, 19-Jan-2025.) |
β’ minPoly = (π β V, π β V β¦ (π₯ β (Baseβπ) β¦ ((idlGen1pβ(π βΎs π))β{π β dom (π evalSub1 π) β£ (((π evalSub1 π)βπ)βπ₯) = (0gβπ)}))) | ||
Theorem | evls1fvcl 33304 | Variant of fveval1fvcl 22239 for the subring evaluation function evalSub1 (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π β π΅) & β’ (π β π β π) β β’ (π β ((πβπ)βπ) β π΅) | ||
Theorem | evls1maprhm 33305* | The function πΉ mapping polynomials π to their subring evaluation at a given point π is a ring homomorphism. (Contributed by Thierry Arnoux, 8-Feb-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π β π΅) & β’ πΉ = (π β π β¦ ((πβπ)βπ)) β β’ (π β πΉ β (π RingHom π )) | ||
Theorem | evls1maplmhm 33306* | The function πΉ mapping polynomials π to their subring evaluation at a given point π΄ is a module homomorphism, when considering the subring algebra. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π β π΅) & β’ πΉ = (π β π β¦ ((πβπ)βπ)) & β’ π΄ = ((subringAlg βπ )βπ) β β’ (π β πΉ β (π LMHom π΄)) | ||
Theorem | evls1maprnss 33307* | The function πΉ mapping polynomials π to their subring evaluation at a given point π΄ takes all values in the subring π. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π β π΅) & β’ πΉ = (π β π β¦ ((πβπ)βπ)) β β’ (π β π β ran πΉ) | ||
Theorem | ply1annidllem 33308* | Write the set π of polynomials annihilating an element π΄ as the kernel of the ring homomorphism πΉ mapping polynomials π to their subring evaluation at a given point π΄. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π΅ = (Baseβπ ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π΄ β π΅) & β’ 0 = (0gβπ ) & β’ π = {π β dom π β£ ((πβπ)βπ΄) = 0 } & β’ πΉ = (π β (Baseβπ) β¦ ((πβπ)βπ΄)) β β’ (π β π = (β‘πΉ β { 0 })) | ||
Theorem | ply1annidl 33309* | The set π of polynomials annihilating an element π΄ forms an ideal. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π΅ = (Baseβπ ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π΄ β π΅) & β’ 0 = (0gβπ ) & β’ π = {π β dom π β£ ((πβπ)βπ΄) = 0 } β β’ (π β π β (LIdealβπ)) | ||
Theorem | ply1annnr 33310* | The set π of polynomials annihilating an element π΄ is not the whole polynomial ring. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π΅ = (Baseβπ ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π΄ β π΅) & β’ 0 = (0gβπ ) & β’ π = {π β dom π β£ ((πβπ)βπ΄) = 0 } & β’ π = (Baseβπ) & β’ (π β π β NzRing) β β’ (π β π β π) | ||
Theorem | ply1annig1p 33311* | The ideal π of polynomials annihilating an element π΄ is generated by the ideal's canonical generator. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1β(πΈ βΎs πΉ)) & β’ π΅ = (BaseβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β π΅) & β’ 0 = (0gβπΈ) & β’ π = {π β dom π β£ ((πβπ)βπ΄) = 0 } & β’ πΎ = (RSpanβπ) & β’ πΊ = (idlGen1pβ(πΈ βΎs πΉ)) β β’ (π β π = (πΎβ{(πΊβπ)})) | ||
Theorem | minplyval 33312* | Expand the value of the minimal polynomial (πβπ΄) for a given element π΄. It is defined as the unique monic polynomial of minimal degree which annihilates π΄. By ply1annig1p 33311, that polynomial generates the ideal of the annihilators of π΄. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1β(πΈ βΎs πΉ)) & β’ π΅ = (BaseβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β π΅) & β’ 0 = (0gβπΈ) & β’ π = {π β dom π β£ ((πβπ)βπ΄) = 0 } & β’ πΎ = (RSpanβπ) & β’ πΊ = (idlGen1pβ(πΈ βΎs πΉ)) & β’ π = (πΈ minPoly πΉ) β β’ (π β (πβπ΄) = (πΊβπ)) | ||
Theorem | minplycl 33313* | The minimal polynomial is a polynomial. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1β(πΈ βΎs πΉ)) & β’ π΅ = (BaseβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β π΅) & β’ 0 = (0gβπΈ) & β’ π = {π β dom π β£ ((πβπ)βπ΄) = 0 } & β’ πΎ = (RSpanβπ) & β’ πΊ = (idlGen1pβ(πΈ βΎs πΉ)) & β’ π = (πΈ minPoly πΉ) β β’ (π β (πβπ΄) β (Baseβπ)) | ||
Theorem | ply1annprmidl 33314* | The set π of polynomials annihilating an element π΄ is a prime ideal. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1β(πΈ βΎs πΉ)) & β’ π΅ = (BaseβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β π΅) & β’ 0 = (0gβπΈ) & β’ π = {π β dom π β£ ((πβπ)βπ΄) = 0 } β β’ (π β π β (PrmIdealβπ)) | ||
Theorem | minplyann 33315 | The minimal polynomial for π΄ annihilates π΄ (Contributed by Thierry Arnoux, 25-Apr-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1β(πΈ βΎs πΉ)) & β’ π΅ = (BaseβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β π΅) & β’ 0 = (0gβπΈ) & β’ π = (πΈ minPoly πΉ) β β’ (π β ((πβ(πβπ΄))βπ΄) = 0 ) | ||
Theorem | minplyirredlem 33316 | Lemma for minplyirred 33317. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1β(πΈ βΎs πΉ)) & β’ π΅ = (BaseβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β π΅) & β’ π = (πΈ minPoly πΉ) & β’ π = (0gβπ) & β’ (π β (πβπ΄) β π) & β’ (π β πΊ β (Baseβπ)) & β’ (π β π» β (Baseβπ)) & β’ (π β (πΊ(.rβπ)π») = (πβπ΄)) & β’ (π β ((πβπΊ)βπ΄) = (0gβπΈ)) & β’ (π β πΊ β π) & β’ (π β π» β π) β β’ (π β π» β (Unitβπ)) | ||
Theorem | minplyirred 33317 | A nonzero minimal polynomial is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1β(πΈ βΎs πΉ)) & β’ π΅ = (BaseβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β π΅) & β’ π = (πΈ minPoly πΉ) & β’ π = (0gβπ) & β’ (π β (πβπ΄) β π) β β’ (π β (πβπ΄) β (Irredβπ)) | ||
Theorem | irngnminplynz 33318 | Integral elements have nonzero minimal polynomials. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π = (0gβ(Poly1βπΈ)) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ π = (πΈ minPoly πΉ) & β’ (π β π΄ β (πΈ IntgRing πΉ)) β β’ (π β (πβπ΄) β π) | ||
Theorem | minplym1p 33319 | A minimal polynomial is monic. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = (0gβ(Poly1βπΈ)) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ π = (πΈ minPoly πΉ) & β’ (π β π΄ β (πΈ IntgRing πΉ)) & β’ π = (Monic1pβ(πΈ βΎs πΉ)) β β’ (π β (πβπ΄) β π) | ||
Theorem | irredminply 33320 | An irreductible, monic, annihilating polynomial is the minimal polynomial. (Contributed by Thierry Arnoux, 27-Apr-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1β(πΈ βΎs πΉ)) & β’ π΅ = (BaseβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β π΅) & β’ 0 = (0gβπΈ) & β’ π = (πΈ minPoly πΉ) & β’ π = (0gβπ) & β’ (π β ((πβπΊ)βπ΄) = 0 ) & β’ (π β πΊ β (Irredβπ)) & β’ (π β πΊ β (Monic1pβ(πΈ βΎs πΉ))) β β’ (π β πΊ = (πβπ΄)) | ||
Theorem | algextdeglem1 33321 | Lemma for algextdeg 33329. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ πΎ = (πΈ βΎs πΉ) & β’ πΏ = (πΈ βΎs (πΈ fldGen (πΉ βͺ {π΄}))) & β’ π· = ( deg1 βπΈ) & β’ π = (πΈ minPoly πΉ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β (πΈ IntgRing πΉ)) β β’ (π β (πΏ βΎs πΉ) = πΎ) | ||
Theorem | algextdeglem2 33322* | Lemma for algextdeg 33329. Both the ring of polynomials π and the field πΏ generated by πΎ and the algebraic element π΄ can be considered as modules over the elements of πΉ. Then, the evaluation map πΊ, mapping polynomials to their evaluation at π΄, is a module homomorphism between those modules. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ πΎ = (πΈ βΎs πΉ) & β’ πΏ = (πΈ βΎs (πΈ fldGen (πΉ βͺ {π΄}))) & β’ π· = ( deg1 βπΈ) & β’ π = (πΈ minPoly πΉ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β (πΈ IntgRing πΉ)) & β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1βπΎ) & β’ π = (Baseβπ) & β’ πΊ = (π β π β¦ ((πβπ)βπ΄)) & β’ π = (π₯ β π β¦ [π₯](π ~QG π)) & β’ π = (β‘πΊ β {(0gβπΏ)}) & β’ π = (π /s (π ~QG π)) & β’ π½ = (π β (Baseβπ) β¦ βͺ (πΊ β π)) β β’ (π β πΊ β (π LMHom ((subringAlg βπΏ)βπΉ))) | ||
Theorem | algextdeglem3 33323* | Lemma for algextdeg 33329. The quotient π / π of the vector space π of polynomials by the subspace π of polynomials annihilating π΄ is itself a vector space. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ πΎ = (πΈ βΎs πΉ) & β’ πΏ = (πΈ βΎs (πΈ fldGen (πΉ βͺ {π΄}))) & β’ π· = ( deg1 βπΈ) & β’ π = (πΈ minPoly πΉ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β (πΈ IntgRing πΉ)) & β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1βπΎ) & β’ π = (Baseβπ) & β’ πΊ = (π β π β¦ ((πβπ)βπ΄)) & β’ π = (π₯ β π β¦ [π₯](π ~QG π)) & β’ π = (β‘πΊ β {(0gβπΏ)}) & β’ π = (π /s (π ~QG π)) & β’ π½ = (π β (Baseβπ) β¦ βͺ (πΊ β π)) β β’ (π β π β LVec) | ||
Theorem | algextdeglem4 33324* | Lemma for algextdeg 33329. By lmhmqusker 33067, the surjective module homomorphism πΊ described in algextdeglem2 33322 induces an isomorphism with the quotient space. Therefore, the dimension of that quotient space π / π is the degree of the algebraic field extension. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ πΎ = (πΈ βΎs πΉ) & β’ πΏ = (πΈ βΎs (πΈ fldGen (πΉ βͺ {π΄}))) & β’ π· = ( deg1 βπΈ) & β’ π = (πΈ minPoly πΉ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β (πΈ IntgRing πΉ)) & β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1βπΎ) & β’ π = (Baseβπ) & β’ πΊ = (π β π β¦ ((πβπ)βπ΄)) & β’ π = (π₯ β π β¦ [π₯](π ~QG π)) & β’ π = (β‘πΊ β {(0gβπΏ)}) & β’ π = (π /s (π ~QG π)) & β’ π½ = (π β (Baseβπ) β¦ βͺ (πΊ β π)) β β’ (π β (dimβπ) = (πΏ[:]πΎ)) | ||
Theorem | algextdeglem5 33325* | Lemma for algextdeg 33329. The subspace π of annihilators of π΄ is a principal ideal generated by the minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ πΎ = (πΈ βΎs πΉ) & β’ πΏ = (πΈ βΎs (πΈ fldGen (πΉ βͺ {π΄}))) & β’ π· = ( deg1 βπΈ) & β’ π = (πΈ minPoly πΉ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β (πΈ IntgRing πΉ)) & β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1βπΎ) & β’ π = (Baseβπ) & β’ πΊ = (π β π β¦ ((πβπ)βπ΄)) & β’ π = (π₯ β π β¦ [π₯](π ~QG π)) & β’ π = (β‘πΊ β {(0gβπΏ)}) & β’ π = (π /s (π ~QG π)) & β’ π½ = (π β (Baseβπ) β¦ βͺ (πΊ β π)) β β’ (π β π = ((RSpanβπ)β{(πβπ΄)})) | ||
Theorem | algextdeglem6 33326* | Lemma for algextdeg 33329. By r1pquslmic 33213, the univariate polynomial remainder ring (π» βs π) is isomorphic with the quotient ring π. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ πΎ = (πΈ βΎs πΉ) & β’ πΏ = (πΈ βΎs (πΈ fldGen (πΉ βͺ {π΄}))) & β’ π· = ( deg1 βπΈ) & β’ π = (πΈ minPoly πΉ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β (πΈ IntgRing πΉ)) & β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1βπΎ) & β’ π = (Baseβπ) & β’ πΊ = (π β π β¦ ((πβπ)βπ΄)) & β’ π = (π₯ β π β¦ [π₯](π ~QG π)) & β’ π = (β‘πΊ β {(0gβπΏ)}) & β’ π = (π /s (π ~QG π)) & β’ π½ = (π β (Baseβπ) β¦ βͺ (πΊ β π)) & β’ π = (rem1pβπΎ) & β’ π» = (π β π β¦ (ππ (πβπ΄))) β β’ (π β (dimβπ) = (dimβ(π» βs π))) | ||
Theorem | algextdeglem7 33327* | Lemma for algextdeg 33329. The polynomials π of lower degree than the minimal polynomial are left unchanged when taking the remainder of the division by that minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ πΎ = (πΈ βΎs πΉ) & β’ πΏ = (πΈ βΎs (πΈ fldGen (πΉ βͺ {π΄}))) & β’ π· = ( deg1 βπΈ) & β’ π = (πΈ minPoly πΉ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β (πΈ IntgRing πΉ)) & β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1βπΎ) & β’ π = (Baseβπ) & β’ πΊ = (π β π β¦ ((πβπ)βπ΄)) & β’ π = (π₯ β π β¦ [π₯](π ~QG π)) & β’ π = (β‘πΊ β {(0gβπΏ)}) & β’ π = (π /s (π ~QG π)) & β’ π½ = (π β (Baseβπ) β¦ βͺ (πΊ β π)) & β’ π = (rem1pβπΎ) & β’ π» = (π β π β¦ (ππ (πβπ΄))) & β’ π = (β‘( deg1 βπΎ) β (-β[,)(π·β(πβπ΄)))) & β’ (π β π β π) β β’ (π β (π β π β (π»βπ) = π)) | ||
Theorem | algextdeglem8 33328* | Lemma for algextdeg 33329. The dimension of the univariate polynomial remainder ring (π» βs π) is the degree of the minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ πΎ = (πΈ βΎs πΉ) & β’ πΏ = (πΈ βΎs (πΈ fldGen (πΉ βͺ {π΄}))) & β’ π· = ( deg1 βπΈ) & β’ π = (πΈ minPoly πΉ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β (πΈ IntgRing πΉ)) & β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1βπΎ) & β’ π = (Baseβπ) & β’ πΊ = (π β π β¦ ((πβπ)βπ΄)) & β’ π = (π₯ β π β¦ [π₯](π ~QG π)) & β’ π = (β‘πΊ β {(0gβπΏ)}) & β’ π = (π /s (π ~QG π)) & β’ π½ = (π β (Baseβπ) β¦ βͺ (πΊ β π)) & β’ π = (rem1pβπΎ) & β’ π» = (π β π β¦ (ππ (πβπ΄))) & β’ π = (β‘( deg1 βπΎ) β (-β[,)(π·β(πβπ΄)))) β β’ (π β (dimβ(π» βs π)) = (π·β(πβπ΄))) | ||
Theorem | algextdeg 33329 | The degree of an algebraic field extension (noted [πΏ:πΎ]) is the degree of the minimal polynomial π(π΄), whereas πΏ is the field generated by πΎ and the algebraic element π΄. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ πΎ = (πΈ βΎs πΉ) & β’ πΏ = (πΈ βΎs (πΈ fldGen (πΉ βͺ {π΄}))) & β’ π· = ( deg1 βπΈ) & β’ π = (πΈ minPoly πΉ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β (πΈ IntgRing πΉ)) β β’ (π β (πΏ[:]πΎ) = (π·β(πβπ΄))) | ||
Syntax | csmat 33330 | Syntax for a function generating submatrices. |
class subMat1 | ||
Definition | df-smat 33331* | 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 22466. (Contributed by Thierry Arnoux, 18-Aug-2020.) |
β’ subMat1 = (π β V β¦ (π β β, π β β β¦ (π β (π β β, π β β β¦ β¨if(π < π, π, (π + 1)), if(π < π, π, (π + 1))β©)))) | ||
Theorem | smatfval 33332* | Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ ((πΎ β β β§ πΏ β β β§ π β π) β (πΎ(subMat1βπ)πΏ) = (π β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) | ||
Theorem | smatrcl 33333 | 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 33334 | Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β β) & β’ (π β π½ β β) & β’ (π β if(πΌ < πΎ, πΌ, (πΌ + 1)) = π) & β’ (π β if(π½ < πΏ, π½, (π½ + 1)) = π) β β’ (π β (πΌππ½) = (ππ΄π)) | ||
Theorem | smattl 33335 | Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β (1..^πΎ)) & β’ (π β π½ β (1..^πΏ)) β β’ (π β (πΌππ½) = (πΌπ΄π½)) | ||
Theorem | smattr 33336 | Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β (πΎ...π)) & β’ (π β π½ β (1..^πΏ)) β β’ (π β (πΌππ½) = ((πΌ + 1)π΄π½)) | ||
Theorem | smatbl 33337 | Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β (1..^πΎ)) & β’ (π β π½ β (πΏ...π)) β β’ (π β (πΌππ½) = (πΌπ΄(π½ + 1))) | ||
Theorem | smatbr 33338 | Entries of a submatrix, bottom right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β (πΎ...π)) & β’ (π β π½ β (πΏ...π)) β β’ (π β (πΌππ½) = ((πΌ + 1)π΄(π½ + 1))) | ||
Theorem | smatcl 33339 | 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 33340* | Write a square matrix as a mapping operation. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) β β’ (π β π΅ β π = (π β π, π β π β¦ (πππ))) | ||
Theorem | 1smat1 33341 | The submatrix of the identity matrix obtained by removing the ith row and the ith column is an identity matrix. Cf. 1marepvsma1 22472. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ 1 = (1rβ((1...π) Mat π )) & β’ (π β π β Ring) & β’ (π β π β β) & β’ (π β πΌ β (1...π)) β β’ (π β (πΌ(subMat1β 1 )πΌ) = (1rβ((1...(π β 1)) Mat π ))) | ||
Theorem | submat1n 33342 | 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 33343 | 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 33344 | Lemma for submateq 33346. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β π β (1...(π β 1))) & β’ (π β πΎ β€ π) β β’ (π β (π β (πΎ...π) β§ (π + 1) β ((1...π) β {πΎ}))) | ||
Theorem | submateqlem2 33345 | Lemma for submateq 33346. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β π β (1...(π β 1))) & β’ (π β π < πΎ) β β’ (π β (π β (1..^πΎ) β§ π β ((1...π) β {πΎ}))) | ||
Theorem | submateq 33346* | 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 33347 | 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 33348 | Extend class notation with the literal matrix conversion function. |
class litMat | ||
Definition | df-lmat 33349* | 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 33350* | Value of the literal matrix conversion function. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ (π β π β (litMatβπ) = (π β (1...(β―βπ)), π β (1...(β―β(πβ0))) β¦ ((πβ(π β 1))β(π β 1)))) | ||
Theorem | lmatfval 33351* | Entries of a literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ π = (litMatβπ) & β’ (π β π β β) & β’ (π β π β Word Word π) & β’ (π β (β―βπ) = π) & β’ ((π β§ π β (0..^π)) β (β―β(πβπ)) = π) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) β β’ (π β (πΌππ½) = ((πβ(πΌ β 1))β(π½ β 1))) | ||
Theorem | lmatfvlem 33352* | 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 33353* | Closure of the literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
β’ π = (litMatβπ) & β’ (π β π β β) & β’ (π β π β Word Word π) & β’ (π β (β―βπ) = π) & β’ ((π β§ π β (0..^π)) β (β―β(πβπ)) = π) & β’ π = (Baseβπ ) & β’ π = ((1...π) Mat π ) & β’ π = (Baseβπ) & β’ (π β π β π) β β’ (π β π β π) | ||
Theorem | lmat22lem 33354* | Lemma for lmat22e11 33355 and co. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ ((π β§ π β (0..^2)) β (β―β(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ)) = 2) | ||
Theorem | lmat22e11 33355 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (1π1) = π΄) | ||
Theorem | lmat22e12 33356 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (1π2) = π΅) | ||
Theorem | lmat22e21 33357 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (2π1) = πΆ) | ||
Theorem | lmat22e22 33358 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (2π2) = π·) | ||
Theorem | lmat22det 33359 | 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 33360* | 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 33361* | 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 33362* | 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 33363* | 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 33364* | Lemma for madjusmdet 33368. (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 33365* | Lemma for madjusmdet 33368. (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 33366* | Lemma for madjusmdet 33368. (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 33367* | Lemma for madjusmdet 33368. (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 33368 | 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 33369* | 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 33370* | The predicate "is a T0 space", using closed sets. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ (π β π΅ = βͺ π½) & β’ (π β π· = (Clsdβπ½)) β β’ (π β (π½ β Kol2 β (π½ β Top β§ βπ₯ β π΅ βπ¦ β π΅ (βπ β π· (π₯ β π β π¦ β π) β π₯ = π¦)))) | ||
Theorem | txomap 33371* | 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 33372* | 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 33373* | 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 33374* | 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 33375* | 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 33376* | 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 10503. (Contributed by Thierry Arnoux, 12-Jan-2020.) |
β’ (π΄ β π β (π΄Refπ΅ β (βͺ π΅ β βͺ π΄ β§ βπ(π:π΄βΆπ΅ β§ βπ£ β π΄ π£ β (πβπ£))))) | ||
Theorem | locfinreflem 33377* | 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 33378* | 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 33379 | The "every open cover has an π΄ refinement" predicate. |
class CovHasRefπ΄ | ||
Definition | df-cref 33380* | 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 33381* | 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 33382 | Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π΄ = π΅ β CovHasRefπ΄ = CovHasRefπ΅) | ||
Theorem | creftop 33383 | A space where every open cover has an π΄ refinement is a topological space. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π½ β CovHasRefπ΄ β π½ β Top) | ||
Theorem | crefi 33384* | The property that every open cover has an π΄ refinement for the topological space π½. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ π = βͺ π½ β β’ ((π½ β CovHasRefπ΄ β§ πΆ β π½ β§ π = βͺ πΆ) β βπ§ β (π« π½ β© π΄)π§RefπΆ) | ||
Theorem | crefdf 33385* | A formulation of crefi 33384 easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ π = βͺ π½ & β’ π΅ = CovHasRefπ΄ & β’ (π§ β π΄ β π) β β’ ((π½ β π΅ β§ πΆ β π½ β§ π = βͺ πΆ) β βπ§ β π« π½(π β§ π§RefπΆ)) | ||
Theorem | crefss 33386 | The "every open cover has an π΄ refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π΄ β π΅ β CovHasRefπ΄ β CovHasRefπ΅) | ||
Theorem | cmpcref 33387 | 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 33388* | Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ π β π½ β§ π = βͺ π) β βπ£ β π« π½(π£ β Fin β§ π£Refπ)) | ||
Syntax | cldlf 33389 | Extend class notation with the class of all LindelΓΆf spaces. |
class Ldlf | ||
Definition | df-ldlf 33390 | 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 33391* | Every open cover of a LindelΓΆf space has a countable refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
β’ π = βͺ π½ β β’ ((π½ β Ldlf β§ π β π½ β§ π = βͺ π) β βπ£ β π« π½(π£ βΌ Ο β§ π£Refπ)) | ||
Syntax | cpcmp 33392 | Extend class notation with the class of all paracompact topologies. |
class Paracomp | ||
Definition | df-pcmp 33393 | 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 33394 | The predicate "is a paracompact topology". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π½ β Paracomp β π½ β CovHasRef(LocFinβπ½)) | ||
Theorem | cmppcmp 33395 | Every compact space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π½ β Comp β π½ β Paracomp) | ||
Theorem | dispcmp 33396 | Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π β π β π« π β Paracomp) | ||
Theorem | pcmplfin 33397* | Given a paracompact topology π½ and an open cover π, there exists an open refinement π£ that is locally finite. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ π = βͺ π½ β β’ ((π½ β Paracomp β§ π β π½ β§ π = βͺ π) β βπ£ β π« π½(π£ β (LocFinβπ½) β§ π£Refπ)) | ||
Theorem | pcmplfinf 33398* | Given a paracompact topology π½ and an open cover π, there exists an open refinement ran π that is locally finite, using the same index as the original cover π. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ π = βͺ π½ β β’ ((π½ β Paracomp β§ π β π½ β§ π = βͺ π) β βπ(π:πβΆπ½ β§ ran πRefπ β§ ran π β (LocFinβπ½))) | ||
The prime ideals of a ring π can be endowed with the Zariski topology. This is done by defining a function π which maps ideals of π to closed sets (see for example zarcls0 33405 for the definition of π). The closed sets of the topology are in the range of π (see zartopon 33414). The correspondence with the open sets is made in zarcls 33411. As proved in zart0 33416, the Zariski topology is T0 , but generally not T1 . | ||
Syntax | crspec 33399 | Extend class notation with the spectrum of a ring. |
class Spec | ||
Definition | df-rspec 33400 | Define the spectrum of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ Spec = (π β Ring β¦ ((IDLsrgβπ) βΎs (PrmIdealβπ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |