![]() |
Metamath
Proof Explorer Theorem List (p. 426 of 483) | < 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-30741) |
![]() (30742-32264) |
![]() (32265-48238) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | islnm 42501* | Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ 𝑆 = (LSubSp‘𝑀) ⇒ ⊢ (𝑀 ∈ LNoeM ↔ (𝑀 ∈ LMod ∧ ∀𝑖 ∈ 𝑆 (𝑀 ↾s 𝑖) ∈ LFinGen)) | ||
Theorem | islnm2 42502* | 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 42503 | A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LMod) | ||
Theorem | lnmlssfg 42504 | A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑀) & ⊢ 𝑅 = (𝑀 ↾s 𝑈) ⇒ ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LFinGen) | ||
Theorem | lnmlsslnm 42505 | All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑀) & ⊢ 𝑅 = (𝑀 ↾s 𝑈) ⇒ ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LNoeM) | ||
Theorem | lnmfg 42506 | A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LFinGen) | ||
Theorem | kercvrlsm 42507 | 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 42508 | 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 42509 | Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵) → 𝑇 ∈ LNoeM) | ||
Theorem | lmhmfgsplit 42510 | 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 42511 | 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 42512 | Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 → (𝑅 ∈ LNoeM ↔ 𝑆 ∈ LNoeM)) | ||
Theorem | pwssplit4 42513* | 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 42514 | Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ Fin) → 𝑊 ∈ LNoeM) | ||
Theorem | pwslnmlem0 42515 | Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s ∅) ⇒ ⊢ (𝑊 ∈ LMod → 𝑌 ∈ LNoeM) | ||
Theorem | pwslnmlem1 42516* | First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s {𝑖}) ⇒ ⊢ (𝑊 ∈ LNoeM → 𝑌 ∈ LNoeM) | ||
Theorem | pwslnmlem2 42517 | 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 42518 | Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s 𝐼) ⇒ ⊢ ((𝑊 ∈ LNoeM ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM) | ||
Theorem | unxpwdom3 42519* | Weaker version of unxpwdom 9613 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 42520* | The pw2f1o 9102 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 42521* | 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 42522 | 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 42523 | Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) |
⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel)) | ||
Theorem | imasgim 42524 | 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 42525 | 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 42526 | The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
⊢ (𝑆 ∈ 𝑉 → (har‘𝑆) ≠ ∅) | ||
Theorem | numinfctb 42527 | A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
⊢ ((𝑆 ∈ dom card ∧ ¬ 𝑆 ∈ Fin) → ω ≼ 𝑆) | ||
Theorem | isnumbasgrplem2 42528 | 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 42529 | 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 42530 | 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 42531 | 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 42532 | 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 42533 | Extend class notation with the class of left Noetherian rings. |
class LNoeR | ||
Definition | df-lnr 42534 | 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 42535 | Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐴 ∈ LNoeR ↔ (𝐴 ∈ Ring ∧ (ringLMod‘𝐴) ∈ LNoeM)) | ||
Theorem | lnrring 42536 | Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐴 ∈ LNoeR → 𝐴 ∈ Ring) | ||
Theorem | lnrlnm 42537 | Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐴 ∈ LNoeR → (ringLMod‘𝐴) ∈ LNoeM) | ||
Theorem | islnr2 42538* | 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 42539 | 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 42540* | 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 42541 | Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝑅 ∈ LPIR → 𝑅 ∈ LNoeR) | ||
Theorem | lnrfrlm 42542 | Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.) |
⊢ 𝑌 = (𝑅 freeLMod 𝐼) ⇒ ⊢ ((𝑅 ∈ LNoeR ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM) | ||
Theorem | lnrfg 42543 | 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 42544 | 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 42545 | The leading ideal sequence used in the Hilbert Basis Theorem. |
class ldgIdlSeq | ||
Definition | df-ldgis 42546* | 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 42554. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}))) | ||
Theorem | hbtlem1 42547* | Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) = {𝑗 ∣ ∃𝑘 ∈ 𝐼 ((𝐷‘𝑘) ≤ 𝑋 ∧ 𝑗 = ((coe1‘𝑘)‘𝑋))}) | ||
Theorem | hbtlem2 42548 | Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝑇 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) ∈ 𝑇) | ||
Theorem | hbtlem7 42549 | Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝑇 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑆‘𝐼):ℕ0⟶𝑇) | ||
Theorem | hbtlem4 42550 | The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) & ⊢ (𝜑 → 𝑌 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐼)‘𝑌)) | ||
Theorem | hbtlem3 42551 | The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐼 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐽)‘𝑋)) | ||
Theorem | hbtlem5 42552* | The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐼 ⊆ 𝐽) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 ((𝑆‘𝐽)‘𝑥) ⊆ ((𝑆‘𝐼)‘𝑥)) ⇒ ⊢ (𝜑 → 𝐼 = 𝐽) | ||
Theorem | hbtlem6 42553* | 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 42554 | 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 42555 | Extend class notation with the class of monic polynomials. |
class Monic | ||
Syntax | cplylt 42556 | Extend class notatin with the class of limited-degree polynomials. |
class Poly< | ||
Definition | df-mnc 42557* | Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1}) | ||
Definition | df-plylt 42558* | Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.) |
⊢ Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)}) | ||
Theorem | dgrsub2 42559 | 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 42560 | Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) ↔ (𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1)) | ||
Theorem | mncply 42561 | A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ∈ (Poly‘𝑆)) | ||
Theorem | mnccoe 42562 | A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) → ((coeff‘𝑃)‘(deg‘𝑃)) = 1) | ||
Theorem | mncn0 42563 | A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ≠ 0𝑝) | ||
Syntax | cdgraa 42564 | Extend class notation to include the degree function for algebraic numbers. |
class degAA | ||
Syntax | cmpaa 42565 | Extend class notation to include the minimal polynomial for an algebraic number. |
class minPolyAA | ||
Definition | df-dgraa 42566* | 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 42567* | 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 42568* | 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 42569* | 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 42570 | Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (degAA‘𝐴) ∈ ℕ) | ||
Theorem | dgraaf 42571 | 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 42572 | 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 42573 | 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 42574* | 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 42575* | 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 42576 | 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 42577 | Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (minPolyAA‘𝐴) ∈ (Poly‘ℚ)) | ||
Theorem | mpaadgr 42578 | Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → (deg‘(minPolyAA‘𝐴)) = (degAA‘𝐴)) | ||
Theorem | mpaaroot 42579 | 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 42580 | Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → ((coeff‘(minPolyAA‘𝐴))‘(degAA‘𝐴)) = 1) | ||
Syntax | citgo 42581 | Extend class notation with the integral-over predicate. |
class IntgOver | ||
Syntax | cza 42582 | Extend class notation with the class of algebraic integers. |
class ℤ | ||
Definition | df-itgo 42583* | A complex number is said to be integral over a subset if it is the root of a monic polynomial with coefficients from the subset. This definition is typically not used for fields but it works there, see aaitgo 42586. This definition could work for subsets of an arbitrary ring with a more general definition of polynomials. TODO: use Monic. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}) | ||
Definition | df-za 42584 | Define an algebraic integer as a complex number which is the root of a monic integer polynomial. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ ℤ = (IntgOver‘ℤ) | ||
Theorem | itgoval 42585* | Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (𝑆 ⊆ ℂ → (IntgOver‘𝑆) = {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑆)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}) | ||
Theorem | aaitgo 42586 | The standard algebraic numbers 𝔸 are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝔸 = (IntgOver‘ℚ) | ||
Theorem | itgoss 42587 | An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (IntgOver‘𝑆) ⊆ (IntgOver‘𝑇)) | ||
Theorem | itgocn 42588 | All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (IntgOver‘𝑆) ⊆ ℂ | ||
Theorem | cnsrexpcl 42589 | Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑋↑𝑌) ∈ 𝑆) | ||
Theorem | fsumcnsrcl 42590* | Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) | ||
Theorem | cnsrplycl 42591 | Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝑃 ∈ (Poly‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝑃‘𝑋) ∈ 𝑆) | ||
Theorem | rgspnval 42592* | Value of the ring-span of a set of elements in a ring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) & ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) ⇒ ⊢ (𝜑 → 𝑈 = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡}) | ||
Theorem | rgspncl 42593 | The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) & ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑅)) | ||
Theorem | rgspnssid 42594 | The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) & ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝑈) | ||
Theorem | rgspnmin 42595 | The ring-span is contained in all subspaces which contain all the generators. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) & ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) ⇒ ⊢ (𝜑 → 𝑈 ⊆ 𝑆) | ||
Theorem | rgspnid 42596 | The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑆 = ((RingSpan‘𝑅)‘𝐴)) ⇒ ⊢ (𝜑 → 𝑆 = 𝐴) | ||
Theorem | rngunsnply 42597* | Adjoining one element to a ring results in a set of polynomial evaluations. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ (𝜑 → 𝐵 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑆 = ((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) ⇒ ⊢ (𝜑 → (𝑉 ∈ 𝑆 ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) | ||
Theorem | flcidc 42598* | Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
⊢ (𝜑 → 𝐹 = (𝑗 ∈ 𝑆 ↦ if(𝑗 = 𝐾, 1, 0))) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑆) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑖 ∈ 𝑆 ((𝐹‘𝑖) · 𝐵) = ⦋𝐾 / 𝑖⦌𝐵) | ||
Syntax | cmend 42599 | Syntax for module endomorphism algebra. |
class MEndo | ||
Definition | df-mend 42600* | Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ MEndo = (𝑚 ∈ V ↦ ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))〉, 〈(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx), (Scalar‘𝑚)〉, 〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))〉})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |