![]() |
Metamath
Proof Explorer Theorem List (p. 419 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | aomclem6 41801* | Lemma for dfac11 41804. Transfinite induction, close over π§. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ π΅ = {β¨π, πβ© β£ βπ β (π 1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π 1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} & β’ πΆ = (π β V β¦ sup((π¦βπ), (π 1βdom π§), π΅)) & β’ π· = recs((π β V β¦ (πΆβ((π 1βdom π§) β ran π)))) & β’ πΈ = {β¨π, πβ© β£ β© (β‘π· β {π}) β β© (β‘π· β {π})} & β’ πΉ = {β¨π, πβ© β£ ((rankβπ) E (rankβπ) β¨ ((rankβπ) = (rankβπ) β§ π(π§βsuc (rankβπ))π))} & β’ πΊ = (if(dom π§ = βͺ dom π§, πΉ, πΈ) β© ((π 1βdom π§) Γ (π 1βdom π§))) & β’ π» = recs((π§ β V β¦ πΊ)) & β’ (π β π΄ β On) & β’ (π β βπ β π« (π 1βπ΄)(π β β β (π¦βπ) β ((π« π β© Fin) β {β }))) β β’ (π β (π»βπ΄) We (π 1βπ΄)) | ||
Theorem | aomclem7 41802* | Lemma for dfac11 41804. (π 1βπ΄) is well-orderable. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ π΅ = {β¨π, πβ© β£ βπ β (π 1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π 1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} & β’ πΆ = (π β V β¦ sup((π¦βπ), (π 1βdom π§), π΅)) & β’ π· = recs((π β V β¦ (πΆβ((π 1βdom π§) β ran π)))) & β’ πΈ = {β¨π, πβ© β£ β© (β‘π· β {π}) β β© (β‘π· β {π})} & β’ πΉ = {β¨π, πβ© β£ ((rankβπ) E (rankβπ) β¨ ((rankβπ) = (rankβπ) β§ π(π§βsuc (rankβπ))π))} & β’ πΊ = (if(dom π§ = βͺ dom π§, πΉ, πΈ) β© ((π 1βdom π§) Γ (π 1βdom π§))) & β’ π» = recs((π§ β V β¦ πΊ)) & β’ (π β π΄ β On) & β’ (π β βπ β π« (π 1βπ΄)(π β β β (π¦βπ) β ((π« π β© Fin) β {β }))) β β’ (π β βπ π We (π 1βπ΄)) | ||
Theorem | aomclem8 41803* | Lemma for dfac11 41804. Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ (π β π΄ β On) & β’ (π β βπ β π« (π 1βπ΄)(π β β β (π¦βπ) β ((π« π β© Fin) β {β }))) β β’ (π β βπ π We (π 1βπ΄)) | ||
Theorem | dfac11 41804* |
The right-hand side of this theorem (compare with ac4 10470),
sometimes
known as the "axiom of multiple choice", is a choice
equivalent.
Curiously, this statement cannot be proved without ax-reg 9587, despite
not mentioning the cumulative hierarchy in any way as most consequences
of regularity do.
This is definition (MC) of [Schechter] p. 141. EDITORIAL: the proof is not original with me of course but I lost my reference sometime after writing it. A multiple choice function allows any total order to be extended to a choice function, which in turn defines a well-ordering. Since a well-ordering on a set defines a simple ordering of the power set, this allows the trivial well-ordering of the empty set to be transfinitely bootstrapped up the cumulative hierarchy to any desired level. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Stefan O'Rear, 1-Jun-2015.) |
β’ (CHOICE β βπ₯βπβπ§ β π₯ (π§ β β β (πβπ§) β ((π« π§ β© Fin) β {β }))) | ||
Theorem | kelac1 41805* | Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((π β§ π₯ β πΌ) β π β β ) & β’ ((π β§ π₯ β πΌ) β π½ β Top) & β’ ((π β§ π₯ β πΌ) β πΆ β (Clsdβπ½)) & β’ ((π β§ π₯ β πΌ) β π΅:πβ1-1-ontoβπΆ) & β’ ((π β§ π₯ β πΌ) β π β βͺ π½) & β’ (π β (βtβ(π₯ β πΌ β¦ π½)) β Comp) β β’ (π β Xπ₯ β πΌ π β β ) | ||
Theorem | kelac2lem 41806 | Lemma for kelac2 41807 and dfac21 41808: knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (π β π β (topGenβ{π, {π« βͺ π}}) β Comp) | ||
Theorem | kelac2 41807* | Kelley's choice, most common form: compactness of a product of knob topologies recovers choice. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((π β§ π₯ β πΌ) β π β π) & β’ ((π β§ π₯ β πΌ) β π β β ) & β’ (π β (βtβ(π₯ β πΌ β¦ (topGenβ{π, {π« βͺ π}}))) β Comp) β β’ (π β Xπ₯ β πΌ π β β ) | ||
Theorem | dfac21 41808 | Tychonoff's theorem is a choice equivalent. Definition AC21 of Schechter p. 461. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro, 27-Aug-2015.) |
β’ (CHOICE β βπ(π:dom πβΆComp β (βtβπ) β Comp)) | ||
Syntax | clfig 41809 | Extend class notation with the class of finitely generated left modules. |
class LFinGen | ||
Definition | df-lfig 41810 | Define the class of finitely generated left modules. Finite generation of subspaces can be intepreted using βΎs. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ LFinGen = {π€ β LMod β£ (Baseβπ€) β ((LSpanβπ€) β (π« (Baseβπ€) β© Fin))} | ||
Theorem | islmodfg 41811* | Property of a finitely generated left module. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π΅ = (Baseβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β (π β LFinGen β βπ β π« π΅(π β Fin β§ (πβπ) = π΅))) | ||
Theorem | islssfg 41812* | Property of a finitely generated left (sub)module. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (π β LFinGen β βπ β π« π(π β Fin β§ (πβπ) = π))) | ||
Theorem | islssfg2 41813* | Property of a finitely generated left (sub)module, with a relaxed constraint on the spanning vectors. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ π΅ = (Baseβπ) β β’ ((π β LMod β§ π β π) β (π β LFinGen β βπ β (π« π΅ β© Fin)(πβπ) = π)) | ||
Theorem | islssfgi 41814 | Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (LSpanβπ) & β’ π = (Baseβπ) & β’ π = (π βΎs (πβπ΅)) β β’ ((π β LMod β§ π΅ β π β§ π΅ β Fin) β π β LFinGen) | ||
Theorem | fglmod 41815 | Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (π β LFinGen β π β LMod) | ||
Theorem | lsmfgcl 41816 | The sum of two finitely generated submodules is finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π· = (π βΎs π΄) & β’ πΈ = (π βΎs π΅) & β’ πΉ = (π βΎs (π΄ β π΅)) & β’ (π β π β LMod) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β LFinGen) & β’ (π β πΈ β LFinGen) β β’ (π β πΉ β LFinGen) | ||
Syntax | clnm 41817 | Extend class notation with the class of Noetherian left modules. |
class LNoeM | ||
Definition | df-lnm 41818* | A left-module is Noetherian iff it is hereditarily finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ LNoeM = {π€ β LMod β£ βπ β (LSubSpβπ€)(π€ βΎs π) β LFinGen} | ||
Theorem | islnm 41819* | Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ π = (LSubSpβπ) β β’ (π β LNoeM β (π β LMod β§ βπ β π (π βΎs π) β LFinGen)) | ||
Theorem | islnm2 41820* | Property of being a Noetherian left module with finite generation expanded in terms of spans. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ (π β LNoeM β (π β LMod β§ βπ β π βπ β (π« π΅ β© Fin)π = (πβπ))) | ||
Theorem | lnmlmod 41821 | A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ (π β LNoeM β π β LMod) | ||
Theorem | lnmlssfg 41822 | A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((π β LNoeM β§ π β π) β π β LFinGen) | ||
Theorem | lnmlsslnm 41823 | All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((π β LNoeM β§ π β π) β π β LNoeM) | ||
Theorem | lnmfg 41824 | A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ (π β LNoeM β π β LFinGen) | ||
Theorem | kercvrlsm 41825 | The domain of a linear function is the subspace sum of the kernel and any subspace which covers the range. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ 0 = (0gβπ) & β’ πΎ = (β‘πΉ β { 0 }) & β’ π΅ = (Baseβπ) & β’ (π β πΉ β (π LMHom π)) & β’ (π β π· β π) & β’ (π β (πΉ β π·) = ran πΉ) β β’ (π β (πΎ β π·) = π΅) | ||
Theorem | lmhmfgima 41826 | A homomorphism maps finitely generated submodules to finitely generated submodules. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βΎs (πΉ β π΄)) & β’ π = (π βΎs π΄) & β’ π = (LSubSpβπ) & β’ (π β π β LFinGen) & β’ (π β π΄ β π) & β’ (π β πΉ β (π LMHom π)) β β’ (π β π β LFinGen) | ||
Theorem | lnmepi 41827 | Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ) β β’ ((πΉ β (π LMHom π) β§ π β LNoeM β§ ran πΉ = π΅) β π β LNoeM) | ||
Theorem | lmhmfgsplit 41828 | If the kernel and range of a homomorphism of left modules are finitely generated, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ 0 = (0gβπ) & β’ πΎ = (β‘πΉ β { 0 }) & β’ π = (π βΎs πΎ) & β’ π = (π βΎs ran πΉ) β β’ ((πΉ β (π LMHom π) β§ π β LFinGen β§ π β LFinGen) β π β LFinGen) | ||
Theorem | lmhmlnmsplit 41829 | If the kernel and range of a homomorphism of left modules are Noetherian, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Revised by Stefan O'Rear, 12-Jun-2015.) |
β’ 0 = (0gβπ) & β’ πΎ = (β‘πΉ β { 0 }) & β’ π = (π βΎs πΎ) & β’ π = (π βΎs ran πΉ) β β’ ((πΉ β (π LMHom π) β§ π β LNoeM β§ π β LNoeM) β π β LNoeM) | ||
Theorem | lnmlmic 41830 | Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β (π β LNoeM β π β LNoeM)) | ||
Theorem | pwssplit4 41831* | Splitting for structure powers 4: maps isomorphically onto the other half. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ πΈ = (π βs (π΄ βͺ π΅)) & β’ πΊ = (BaseβπΈ) & β’ 0 = (0gβπ ) & β’ πΎ = {π¦ β πΊ β£ (π¦ βΎ π΄) = (π΄ Γ { 0 })} & β’ πΉ = (π₯ β πΎ β¦ (π₯ βΎ π΅)) & β’ πΆ = (π βs π΄) & β’ π· = (π βs π΅) & β’ πΏ = (πΈ βΎs πΎ) β β’ ((π β LMod β§ (π΄ βͺ π΅) β π β§ (π΄ β© π΅) = β ) β πΉ β (πΏ LMIso π·)) | ||
Theorem | filnm 41832 | Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ) β β’ ((π β LMod β§ π΅ β Fin) β π β LNoeM) | ||
Theorem | pwslnmlem0 41833 | Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs β ) β β’ (π β LMod β π β LNoeM) | ||
Theorem | pwslnmlem1 41834* | First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs {π}) β β’ (π β LNoeM β π β LNoeM) | ||
Theorem | pwslnmlem2 41835 | A sum of powers is Noetherian. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ π΄ β V & β’ π΅ β V & β’ π = (π βs π΄) & β’ π = (π βs π΅) & β’ π = (π βs (π΄ βͺ π΅)) & β’ (π β π β LMod) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β π β LNoeM) & β’ (π β π β LNoeM) β β’ (π β π β LNoeM) | ||
Theorem | pwslnm 41836 | Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β LNoeM β§ πΌ β Fin) β π β LNoeM) | ||
Theorem | unxpwdom3 41837* | Weaker version of unxpwdom 9584 where a function is required only to be cancellative, not an injection. π· and π΅ are to be thought of as "large" "horizonal" sets, the others as "small". Because the operator is row-wise injective, but the whole row cannot inject into π΄, each row must hit an element of π΅; by column injectivity, each row can be identified in at least one way by the π΅ element that it hits and the column in which it is hit. (Contributed by Stefan O'Rear, 8-Jul-2015.) MOVABLE |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β π) & β’ ((π β§ π β πΆ β§ π β π·) β (π + π) β (π΄ βͺ π΅)) & β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π·)) β ((π + π) = (π + π) β π = π)) & β’ (((π β§ π β π·) β§ (π β πΆ β§ π β πΆ)) β ((π + π) = (π + π) β π = π)) & β’ (π β Β¬ π· βΌ π΄) β β’ (π β πΆ βΌ* (π· Γ π΅)) | ||
Theorem | pwfi2f1o 41838* | The pw2f1o 9077 bijection relates finitely supported indicator functions on a two-element set to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.) |
β’ π = {π¦ β (2o βm π΄) β£ π¦ finSupp β } & β’ πΉ = (π₯ β π β¦ (β‘π₯ β {1o})) β β’ (π΄ β π β πΉ:πβ1-1-ontoβ(π« π΄ β© Fin)) | ||
Theorem | pwfi2en 41839* | Finitely supported indicator functions are equinumerous to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.) |
β’ π = {π¦ β (2o βm π΄) β£ π¦ finSupp β } β β’ (π΄ β π β π β (π« π΄ β© Fin)) | ||
Theorem | frlmpwfi 41840 | Formal linear combinations over Z/2Z are equivalent to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Proof shortened by AV, 14-Jun-2020.) |
β’ π = (β€/nβ€β2) & β’ π = (π freeLMod πΌ) & β’ π΅ = (Baseβπ) β β’ (πΌ β π β π΅ β (π« πΌ β© Fin)) | ||
Theorem | gicabl 41841 | Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) |
β’ (πΊ βπ π» β (πΊ β Abel β π» β Abel)) | ||
Theorem | imasgim 41842 | A relabeling of the elements of a group induces an isomorphism to the relabeled group. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) (Revised by Mario Carneiro, 11-Aug-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβ1-1-ontoβπ΅) & β’ (π β π β Grp) β β’ (π β πΉ β (π GrpIso π)) | ||
Theorem | isnumbasgrplem1 41843 | A set which is equipollent to the base set of a definable Abelian group is the base set of some (relabeled) Abelian group. (Contributed by Stefan O'Rear, 8-Jul-2015.) |
β’ π΅ = (Baseβπ ) β β’ ((π β Abel β§ πΆ β π΅) β πΆ β (Base β Abel)) | ||
Theorem | harn0 41844 | The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ (π β π β (harβπ) β β ) | ||
Theorem | numinfctb 41845 | A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ ((π β dom card β§ Β¬ π β Fin) β Ο βΌ π) | ||
Theorem | isnumbasgrplem2 41846 | If the (to be thought of as disjoint, although the proof does not require this) union of a set and its Hartogs number supports a group structure (more generally, a cancellative magma), then the set must be numerable. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ ((π βͺ (harβπ)) β (Base β Grp) β π β dom card) | ||
Theorem | isnumbasgrplem3 41847 | Every nonempty numerable set can be given the structure of an Abelian group, either a finite cyclic group or a vector space over Z/2Z. (Contributed by Stefan O'Rear, 10-Jul-2015.) |
β’ ((π β dom card β§ π β β ) β π β (Base β Abel)) | ||
Theorem | isnumbasabl 41848 | A set is numerable iff it and its Hartogs number can be jointly given the structure of an Abelian group. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ (π β dom card β (π βͺ (harβπ)) β (Base β Abel)) | ||
Theorem | isnumbasgrp 41849 | A set is numerable iff it and its Hartogs number can be jointly given the structure of a group. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ (π β dom card β (π βͺ (harβπ)) β (Base β Grp)) | ||
Theorem | dfacbasgrp 41850 | A choice equivalent in abstract algebra: All nonempty sets admit a group structure. From http://mathoverflow.net/a/12988. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ (CHOICE β (Base β Grp) = (V β {β })) | ||
Syntax | clnr 41851 | Extend class notation with the class of left Noetherian rings. |
class LNoeR | ||
Definition | df-lnr 41852 | A ring is left-Noetherian iff it is Noetherian as a left module over itself. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ LNoeR = {π β Ring β£ (ringLModβπ) β LNoeM} | ||
Theorem | islnr 41853 | Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π΄ β LNoeR β (π΄ β Ring β§ (ringLModβπ΄) β LNoeM)) | ||
Theorem | lnrring 41854 | Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π΄ β LNoeR β π΄ β Ring) | ||
Theorem | lnrlnm 41855 | Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π΄ β LNoeR β (ringLModβπ΄) β LNoeM) | ||
Theorem | islnr2 41856* | Property of being a left-Noetherian ring in terms of finite generation of ideals (the usual "pure ring theory" definition). (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (LIdealβπ ) & β’ π = (RSpanβπ ) β β’ (π β LNoeR β (π β Ring β§ βπ β π βπ β (π« π΅ β© Fin)π = (πβπ))) | ||
Theorem | islnr3 41857 | Relate left-Noetherian rings to Noetherian-type closure property of the left ideal system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (LIdealβπ ) β β’ (π β LNoeR β (π β Ring β§ π β (NoeACSβπ΅))) | ||
Theorem | lnr2i 41858* | Given an ideal in a left-Noetherian ring, there is a finite subset which generates it. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ π = (LIdealβπ ) & β’ π = (RSpanβπ ) β β’ ((π β LNoeR β§ πΌ β π) β βπ β (π« πΌ β© Fin)πΌ = (πβπ)) | ||
Theorem | lpirlnr 41859 | Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π β LPIR β π β LNoeR) | ||
Theorem | lnrfrlm 41860 | Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.) |
β’ π = (π freeLMod πΌ) β β’ ((π β LNoeR β§ πΌ β Fin) β π β LNoeM) | ||
Theorem | lnrfg 41861 | Finitely-generated modules over a Noetherian ring, being homomorphic images of free modules, are Noetherian. (Contributed by Stefan O'Rear, 7-Feb-2015.) |
β’ π = (Scalarβπ) β β’ ((π β LFinGen β§ π β LNoeR) β π β LNoeM) | ||
Theorem | lnrfgtr 41862 | A submodule of a finitely generated module over a Noetherian ring is finitely generated. Often taken as the definition of Noetherian ring. (Contributed by Stefan O'Rear, 7-Feb-2015.) |
β’ π = (Scalarβπ) & β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((π β LFinGen β§ π β LNoeR β§ π β π) β π β LFinGen) | ||
Syntax | cldgis 41863 | The leading ideal sequence used in the Hilbert Basis Theorem. |
class ldgIdlSeq | ||
Definition | df-ldgis 41864* | Define a function which carries polynomial ideals to the sequence of coefficient ideals of leading coefficients of degree- π₯ elements in the polynomial ideal. The proof that this map is strictly monotone is the core of the Hilbert Basis Theorem hbt 41872. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ ldgIdlSeq = (π β V β¦ (π β (LIdealβ(Poly1βπ)) β¦ (π₯ β β0 β¦ {π β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))) | ||
Theorem | hbtlem1 41865* | Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ π· = ( deg1 βπ ) β β’ ((π β π β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((π·βπ) β€ π β§ π = ((coe1βπ)βπ))}) | ||
Theorem | hbtlem2 41866 | Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) β π) | ||
Theorem | hbtlem7 41867 | Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π) β (πβπΌ):β0βΆπ) | ||
Theorem | hbtlem4 41868 | The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β π β€ π) β β’ (π β ((πβπΌ)βπ) β ((πβπΌ)βπ)) | ||
Theorem | hbtlem3 41869 | The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π½ β π) & β’ (π β πΌ β π½) & β’ (π β π β β0) β β’ (π β ((πβπΌ)βπ) β ((πβπ½)βπ)) | ||
Theorem | hbtlem5 41870* | The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π½ β π) & β’ (π β πΌ β π½) & β’ (π β βπ₯ β β0 ((πβπ½)βπ₯) β ((πβπΌ)βπ₯)) β β’ (π β πΌ = π½) | ||
Theorem | hbtlem6 41871* | There is a finite set of polynomials matching any single stage of the image. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ π = (RSpanβπ) & β’ (π β π β LNoeR) & β’ (π β πΌ β π) & β’ (π β π β β0) β β’ (π β βπ β (π« πΌ β© Fin)((πβπΌ)βπ) β ((πβ(πβπ))βπ)) | ||
Theorem | hbt 41872 | The Hilbert Basis Theorem - the ring of univariate polynomials over a Noetherian ring is a Noetherian ring. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π = (Poly1βπ ) β β’ (π β LNoeR β π β LNoeR) | ||
Syntax | cmnc 41873 | Extend class notation with the class of monic polynomials. |
class Monic | ||
Syntax | cplylt 41874 | Extend class notatin with the class of limited-degree polynomials. |
class Poly< | ||
Definition | df-mnc 41875* | Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ Monic = (π β π« β β¦ {π β (Polyβπ ) β£ ((coeffβπ)β(degβπ)) = 1}) | ||
Definition | df-plylt 41876* | Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.) |
β’ Poly< = (π β π« β, π₯ β β0 β¦ {π β (Polyβπ ) β£ (π = 0π β¨ (degβπ) < π₯)}) | ||
Theorem | dgrsub2 41877 | Subtracting two polynomials with the same degree and top coefficient gives a polynomial of strictly lower degree. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ π = (degβπΉ) β β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ ((degβπΊ) = π β§ π β β β§ ((coeffβπΉ)βπ) = ((coeffβπΊ)βπ))) β (degβ(πΉ βf β πΊ)) < π) | ||
Theorem | elmnc 41878 | Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β ( Monic βπ) β (π β (Polyβπ) β§ ((coeffβπ)β(degβπ)) = 1)) | ||
Theorem | mncply 41879 | A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β ( Monic βπ) β π β (Polyβπ)) | ||
Theorem | mnccoe 41880 | A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β ( Monic βπ) β ((coeffβπ)β(degβπ)) = 1) | ||
Theorem | mncn0 41881 | A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β ( Monic βπ) β π β 0π) | ||
Syntax | cdgraa 41882 | Extend class notation to include the degree function for algebraic numbers. |
class degAA | ||
Syntax | cmpaa 41883 | Extend class notation to include the minimal polynomial for an algebraic number. |
class minPolyAA | ||
Definition | df-dgraa 41884* | Define the degree of an algebraic number as the smallest degree of any nonzero polynomial which has said number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Revised by AV, 29-Sep-2020.) |
β’ degAA = (π₯ β πΈ β¦ inf({π β β β£ βπ β ((Polyββ) β {0π})((degβπ) = π β§ (πβπ₯) = 0)}, β, < )) | ||
Definition | df-mpaa 41885* | Define the minimal polynomial of an algebraic number as the unique monic polynomial which achieves the minimum of degAA. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ minPolyAA = (π₯ β πΈ β¦ (β©π β (Polyββ)((degβπ) = (degAAβπ₯) β§ (πβπ₯) = 0 β§ ((coeffβπ)β(degAAβπ₯)) = 1))) | ||
Theorem | dgraaval 41886* | Value of the degree function on an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Revised by AV, 29-Sep-2020.) |
β’ (π΄ β πΈ β (degAAβπ΄) = inf({π β β β£ βπ β ((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)}, β, < )) | ||
Theorem | dgraalem 41887* | Properties of the degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
β’ (π΄ β πΈ β ((degAAβπ΄) β β β§ βπ β ((Polyββ) β {0π})((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0))) | ||
Theorem | dgraacl 41888 | Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β (degAAβπ΄) β β) | ||
Theorem | dgraaf 41889 | Degree function on algebraic numbers is a function. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
β’ degAA:πΈβΆβ | ||
Theorem | dgraaub 41890 | Upper bound on degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
β’ (((π β (Polyββ) β§ π β 0π) β§ (π΄ β β β§ (πβπ΄) = 0)) β (degAAβπ΄) β€ (degβπ)) | ||
Theorem | dgraa0p 41891 | A rational polynomial of degree less than an algebraic number cannot be zero at that number unless it is the zero polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ ((π΄ β πΈ β§ π β (Polyββ) β§ (degβπ) < (degAAβπ΄)) β ((πβπ΄) = 0 β π = 0π)) | ||
Theorem | mpaaeu 41892* | An algebraic number has exactly one monic polynomial of the least degree. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β β!π β (Polyββ)((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0 β§ ((coeffβπ)β(degAAβπ΄)) = 1)) | ||
Theorem | mpaaval 41893* | Value of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β (minPolyAAβπ΄) = (β©π β (Polyββ)((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0 β§ ((coeffβπ)β(degAAβπ΄)) = 1))) | ||
Theorem | mpaalem 41894 | Properties of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β ((minPolyAAβπ΄) β (Polyββ) β§ ((degβ(minPolyAAβπ΄)) = (degAAβπ΄) β§ ((minPolyAAβπ΄)βπ΄) = 0 β§ ((coeffβ(minPolyAAβπ΄))β(degAAβπ΄)) = 1))) | ||
Theorem | mpaacl 41895 | Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β (minPolyAAβπ΄) β (Polyββ)) | ||
Theorem | mpaadgr 41896 | Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β (degβ(minPolyAAβπ΄)) = (degAAβπ΄)) | ||
Theorem | mpaaroot 41897 | The minimal polynomial of an algebraic number has the number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β ((minPolyAAβπ΄)βπ΄) = 0) | ||
Theorem | mpaamn 41898 | Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β ((coeffβ(minPolyAAβπ΄))β(degAAβπ΄)) = 1) | ||
Syntax | citgo 41899 | Extend class notation with the integral-over predicate. |
class IntgOver | ||
Syntax | cza 41900 | Extend class notation with the class of algebraic integers. |
class β€ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |