Home | Metamath
Proof Explorer Theorem List (p. 413 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | weeq12d 41201 | Equality deduction for well-orders. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π β π = π) & β’ (π β π΄ = π΅) β β’ (π β (π We π΄ β π We π΅)) | ||
Theorem | limsuc2 41202 | Limit ordinals in the sense inclusive of zero contain all successors of their members. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ ((Ord π΄ β§ π΄ = βͺ π΄) β (π΅ β π΄ β suc π΅ β π΄)) | ||
Theorem | wepwsolem 41203* | Transfer an ordering on characteristic functions by isomorphism to the power set. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π§ β π¦ β§ Β¬ π§ β π₯) β§ βπ€ β π΄ (π€π π§ β (π€ β π₯ β π€ β π¦)))} & β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§) E (π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} & β’ πΉ = (π β (2o βm π΄) β¦ (β‘π β {1o})) β β’ (π΄ β V β πΉ Isom π, π ((2o βm π΄), π« π΄)) | ||
Theorem | wepwso 41204* | A well-ordering induces a strict ordering on the power set. EDITORIAL: when well-orderings are set like, this can be strengthened to remove π΄ β π. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π§ β π¦ β§ Β¬ π§ β π₯) β§ βπ€ β π΄ (π€π π§ β (π€ β π₯ β π€ β π¦)))} β β’ ((π΄ β π β§ π We π΄) β π Or π« π΄) | ||
Theorem | dnnumch1 41205* | Define an enumeration of a set from a choice function; second part, it restricts to a bijection. EDITORIAL: overlaps dfac8a 9900. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) β β’ (π β βπ₯ β On (πΉ βΎ π₯):π₯β1-1-ontoβπ΄) | ||
Theorem | dnnumch2 41206* | Define an enumeration (weak dominance version) of a set from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) β β’ (π β π΄ β ran πΉ) | ||
Theorem | dnnumch3lem 41207* | Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) β β’ ((π β§ π€ β π΄) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) = β© (β‘πΉ β {π€})) | ||
Theorem | dnnumch3 41208* | Define an injection from a set into the ordinals using a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) β β’ (π β (π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄β1-1βOn) | ||
Theorem | dnwech 41209* | Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) & β’ π» = {β¨π£, π€β© β£ β© (β‘πΉ β {π£}) β β© (β‘πΉ β {π€})} β β’ (π β π» We π΄) | ||
Theorem | fnwe2val 41210* | Lemma for fnwe2 41214. Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} β β’ (πππ β ((πΉβπ)π (πΉβπ) β¨ ((πΉβπ) = (πΉβπ) β§ πβ¦(πΉβπ) / π§β¦ππ))) | ||
Theorem | fnwe2lem1 41211* | Lemma for fnwe2 41214. Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} & β’ ((π β§ π₯ β π΄) β π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ₯)}) β β’ ((π β§ π β π΄) β β¦(πΉβπ) / π§β¦π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ)}) | ||
Theorem | fnwe2lem2 41212* | Lemma for fnwe2 41214. An element which is in a minimal fiber and minimal within its fiber is minimal globally; thus π is well-founded. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} & β’ ((π β§ π₯ β π΄) β π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ₯)}) & β’ (π β (πΉ βΎ π΄):π΄βΆπ΅) & β’ (π β π We π΅) & β’ (π β π β π΄) & β’ (π β π β β ) β β’ (π β βπ β π βπ β π Β¬ πππ) | ||
Theorem | fnwe2lem3 41213* | Lemma for fnwe2 41214. Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} & β’ ((π β§ π₯ β π΄) β π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ₯)}) & β’ (π β (πΉ βΎ π΄):π΄βΆπ΅) & β’ (π β π We π΅) & β’ (π β π β π΄) & β’ (π β π β π΄) β β’ (π β (πππ β¨ π = π β¨ πππ)) | ||
Theorem | fnwe2 41214* | A well-ordering can be constructed on a partitioned set by patching together well-orderings on each partition using a well-ordering on the partitions themselves. Similar to fnwe 8053 but does not require the within-partition ordering to be globally well. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} & β’ ((π β§ π₯ β π΄) β π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ₯)}) & β’ (π β (πΉ βΎ π΄):π΄βΆπ΅) & β’ (π β π We π΅) β β’ (π β π We π΄) | ||
Theorem | aomclem1 41215* |
Lemma for dfac11 41223. This is the beginning of the proof that
multiple
choice is equivalent to choice. Our goal is to construct, by
transfinite recursion, a well-ordering of (π
1βπ΄). In what
follows, π΄ is the index of the rank we wish to
well-order, π§ is
the collection of well-orderings constructed so far, dom π§ is
the
set of ordinal indices of constructed ranks i.e. the next rank to
construct, and π¦ is a postulated multiple-choice
function.
Successor case 1, define a simple ordering from the well-ordered predecessor. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ π΅ = {β¨π, πβ© β£ βπ β (π 1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π 1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} & β’ (π β dom π§ β On) & β’ (π β dom π§ = suc βͺ dom π§) & β’ (π β βπ β dom π§(π§βπ) We (π 1βπ)) β β’ (π β π΅ Or (π 1βdom π§)) | ||
Theorem | aomclem2 41216* | Lemma for dfac11 41223. Successor case 2, a choice function for subsets of (π 1βdom π§). (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ π΅ = {β¨π, πβ© β£ βπ β (π 1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π 1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} & β’ πΆ = (π β V β¦ sup((π¦βπ), (π 1βdom π§), π΅)) & β’ (π β dom π§ β On) & β’ (π β dom π§ = suc βͺ dom π§) & β’ (π β βπ β dom π§(π§βπ) We (π 1βπ)) & β’ (π β π΄ β On) & β’ (π β dom π§ β π΄) & β’ (π β βπ β π« (π 1βπ΄)(π β β β (π¦βπ) β ((π« π β© Fin) β {β }))) β β’ (π β βπ β π« (π 1βdom π§)(π β β β (πΆβπ) β π)) | ||
Theorem | aomclem3 41217* | Lemma for dfac11 41223. Successor case 3, our required well-ordering. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ π΅ = {β¨π, πβ© β£ βπ β (π 1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π 1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} & β’ πΆ = (π β V β¦ sup((π¦βπ), (π 1βdom π§), π΅)) & β’ π· = recs((π β V β¦ (πΆβ((π 1βdom π§) β ran π)))) & β’ πΈ = {β¨π, πβ© β£ β© (β‘π· β {π}) β β© (β‘π· β {π})} & β’ (π β dom π§ β On) & β’ (π β dom π§ = suc βͺ dom π§) & β’ (π β βπ β dom π§(π§βπ) We (π 1βπ)) & β’ (π β π΄ β On) & β’ (π β dom π§ β π΄) & β’ (π β βπ β π« (π 1βπ΄)(π β β β (π¦βπ) β ((π« π β© Fin) β {β }))) β β’ (π β πΈ We (π 1βdom π§)) | ||
Theorem | aomclem4 41218* | Lemma for dfac11 41223. Limit case. Patch together well-orderings constructed so far using fnwe2 41214 to cover the limit rank. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ πΉ = {β¨π, πβ© β£ ((rankβπ) E (rankβπ) β¨ ((rankβπ) = (rankβπ) β§ π(π§βsuc (rankβπ))π))} & β’ (π β dom π§ β On) & β’ (π β dom π§ = βͺ dom π§) & β’ (π β βπ β dom π§(π§βπ) We (π 1βπ)) β β’ (π β πΉ We (π 1βdom π§)) | ||
Theorem | aomclem5 41219* | Lemma for dfac11 41223. Combine the successor case with the limit case. (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 π§))) & β’ (π β dom π§ β On) & β’ (π β βπ β dom π§(π§βπ) We (π 1βπ)) & β’ (π β π΄ β On) & β’ (π β dom π§ β π΄) & β’ (π β βπ β π« (π 1βπ΄)(π β β β (π¦βπ) β ((π« π β© Fin) β {β }))) β β’ (π β πΊ We (π 1βdom π§)) | ||
Theorem | aomclem6 41220* | Lemma for dfac11 41223. 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 41221* | Lemma for dfac11 41223. (π 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 41222* | Lemma for dfac11 41223. 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 41223* |
The right-hand side of this theorem (compare with ac4 10345),
sometimes
known as the "axiom of multiple choice", is a choice
equivalent.
Curiously, this statement cannot be proved without ax-reg 9462, 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 41224* | 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 41225 | Lemma for kelac2 41226 and dfac21 41227: knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (π β π β (topGenβ{π, {π« βͺ π}}) β Comp) | ||
Theorem | kelac2 41226* | 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 41227 | 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 41228 | Extend class notation with the class of finitely generated left modules. |
class LFinGen | ||
Definition | df-lfig 41229 | 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 41230* | Property of a finitely generated left module. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π΅ = (Baseβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β (π β LFinGen β βπ β π« π΅(π β Fin β§ (πβπ) = π΅))) | ||
Theorem | islssfg 41231* | Property of a finitely generated left (sub)module. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (π β LFinGen β βπ β π« π(π β Fin β§ (πβπ) = π))) | ||
Theorem | islssfg2 41232* | 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 41233 | Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (LSpanβπ) & β’ π = (Baseβπ) & β’ π = (π βΎs (πβπ΅)) β β’ ((π β LMod β§ π΅ β π β§ π΅ β Fin) β π β LFinGen) | ||
Theorem | fglmod 41234 | Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (π β LFinGen β π β LMod) | ||
Theorem | lsmfgcl 41235 | 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 41236 | Extend class notation with the class of Noetherian left modules. |
class LNoeM | ||
Definition | df-lnm 41237* | 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 41238* | Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ π = (LSubSpβπ) β β’ (π β LNoeM β (π β LMod β§ βπ β π (π βΎs π) β LFinGen)) | ||
Theorem | islnm2 41239* | 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 41240 | A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ (π β LNoeM β π β LMod) | ||
Theorem | lnmlssfg 41241 | A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((π β LNoeM β§ π β π) β π β LFinGen) | ||
Theorem | lnmlsslnm 41242 | All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((π β LNoeM β§ π β π) β π β LNoeM) | ||
Theorem | lnmfg 41243 | A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ (π β LNoeM β π β LFinGen) | ||
Theorem | kercvrlsm 41244 | 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 41245 | 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 41246 | Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ) β β’ ((πΉ β (π LMHom π) β§ π β LNoeM β§ ran πΉ = π΅) β π β LNoeM) | ||
Theorem | lmhmfgsplit 41247 | 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 41248 | 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 41249 | Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β (π β LNoeM β π β LNoeM)) | ||
Theorem | pwssplit4 41250* | 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 41251 | Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ) β β’ ((π β LMod β§ π΅ β Fin) β π β LNoeM) | ||
Theorem | pwslnmlem0 41252 | Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs β ) β β’ (π β LMod β π β LNoeM) | ||
Theorem | pwslnmlem1 41253* | First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs {π}) β β’ (π β LNoeM β π β LNoeM) | ||
Theorem | pwslnmlem2 41254 | 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 41255 | Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β LNoeM β§ πΌ β Fin) β π β LNoeM) | ||
Theorem | unxpwdom3 41256* | Weaker version of unxpwdom 9459 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 41257* | The pw2f1o 8955 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 41258* | 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 41259 | 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 41260 | Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) |
β’ (πΊ βπ π» β (πΊ β Abel β π» β Abel)) | ||
Theorem | imasgim 41261 | 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 41262 | 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 41263 | The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ (π β π β (harβπ) β β ) | ||
Theorem | numinfctb 41264 | A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ ((π β dom card β§ Β¬ π β Fin) β Ο βΌ π) | ||
Theorem | isnumbasgrplem2 41265 | 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 41266 | 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 41267 | 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 41268 | 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 41269 | 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 41270 | Extend class notation with the class of left Noetherian rings. |
class LNoeR | ||
Definition | df-lnr 41271 | 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 41272 | Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π΄ β LNoeR β (π΄ β Ring β§ (ringLModβπ΄) β LNoeM)) | ||
Theorem | lnrring 41273 | Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π΄ β LNoeR β π΄ β Ring) | ||
Theorem | lnrlnm 41274 | Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π΄ β LNoeR β (ringLModβπ΄) β LNoeM) | ||
Theorem | islnr2 41275* | 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 41276 | 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 41277* | 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 41278 | Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π β LPIR β π β LNoeR) | ||
Theorem | lnrfrlm 41279 | Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.) |
β’ π = (π freeLMod πΌ) β β’ ((π β LNoeR β§ πΌ β Fin) β π β LNoeM) | ||
Theorem | lnrfg 41280 | 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 41281 | 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 41282 | The leading ideal sequence used in the Hilbert Basis Theorem. |
class ldgIdlSeq | ||
Definition | df-ldgis 41283* | 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 41291. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ ldgIdlSeq = (π β V β¦ (π β (LIdealβ(Poly1βπ)) β¦ (π₯ β β0 β¦ {π β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))) | ||
Theorem | hbtlem1 41284* | Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ π· = ( deg1 βπ ) β β’ ((π β π β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((π·βπ) β€ π β§ π = ((coe1βπ)βπ))}) | ||
Theorem | hbtlem2 41285 | Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) β π) | ||
Theorem | hbtlem7 41286 | Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π) β (πβπΌ):β0βΆπ) | ||
Theorem | hbtlem4 41287 | The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β π β€ π) β β’ (π β ((πβπΌ)βπ) β ((πβπΌ)βπ)) | ||
Theorem | hbtlem3 41288 | The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π½ β π) & β’ (π β πΌ β π½) & β’ (π β π β β0) β β’ (π β ((πβπΌ)βπ) β ((πβπ½)βπ)) | ||
Theorem | hbtlem5 41289* | The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π½ β π) & β’ (π β πΌ β π½) & β’ (π β βπ₯ β β0 ((πβπ½)βπ₯) β ((πβπΌ)βπ₯)) β β’ (π β πΌ = π½) | ||
Theorem | hbtlem6 41290* | 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 41291 | 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 41292 | Extend class notation with the class of monic polynomials. |
class Monic | ||
Syntax | cplylt 41293 | Extend class notatin with the class of limited-degree polynomials. |
class Poly< | ||
Definition | df-mnc 41294* | Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ Monic = (π β π« β β¦ {π β (Polyβπ ) β£ ((coeffβπ)β(degβπ)) = 1}) | ||
Definition | df-plylt 41295* | Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.) |
β’ Poly< = (π β π« β, π₯ β β0 β¦ {π β (Polyβπ ) β£ (π = 0π β¨ (degβπ) < π₯)}) | ||
Theorem | dgrsub2 41296 | 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 41297 | Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β ( Monic βπ) β (π β (Polyβπ) β§ ((coeffβπ)β(degβπ)) = 1)) | ||
Theorem | mncply 41298 | A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β ( Monic βπ) β π β (Polyβπ)) | ||
Theorem | mnccoe 41299 | A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β ( Monic βπ) β ((coeffβπ)β(degβπ)) = 1) | ||
Theorem | mncn0 41300 | A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β ( Monic βπ) β π β 0π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |