| Metamath
Proof Explorer Theorem List (p. 432 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | pwssplit4 43101* | 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 43102 | Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ Fin) → 𝑊 ∈ LNoeM) | ||
| Theorem | pwslnmlem0 43103 | Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
| ⊢ 𝑌 = (𝑊 ↑s ∅) ⇒ ⊢ (𝑊 ∈ LMod → 𝑌 ∈ LNoeM) | ||
| Theorem | pwslnmlem1 43104* | First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
| ⊢ 𝑌 = (𝑊 ↑s {𝑖}) ⇒ ⊢ (𝑊 ∈ LNoeM → 𝑌 ∈ LNoeM) | ||
| Theorem | pwslnmlem2 43105 | 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 43106 | Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
| ⊢ 𝑌 = (𝑊 ↑s 𝐼) ⇒ ⊢ ((𝑊 ∈ LNoeM ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM) | ||
| Theorem | unxpwdom3 43107* | Weaker version of unxpwdom 9629 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 43108* | The pw2f1o 9117 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 43109* | 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 43110 | 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 43111 | Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) |
| ⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel)) | ||
| Theorem | imasgim 43112 | 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 43113 | 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 43114 | The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
| ⊢ (𝑆 ∈ 𝑉 → (har‘𝑆) ≠ ∅) | ||
| Theorem | numinfctb 43115 | A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
| ⊢ ((𝑆 ∈ dom card ∧ ¬ 𝑆 ∈ Fin) → ω ≼ 𝑆) | ||
| Theorem | isnumbasgrplem2 43116 | 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 43117 | 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 43118 | 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 43119 | 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 43120 | 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 43121 | Extend class notation with the class of left Noetherian rings. |
| class LNoeR | ||
| Definition | df-lnr 43122 | 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 43123 | Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
| ⊢ (𝐴 ∈ LNoeR ↔ (𝐴 ∈ Ring ∧ (ringLMod‘𝐴) ∈ LNoeM)) | ||
| Theorem | lnrring 43124 | Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
| ⊢ (𝐴 ∈ LNoeR → 𝐴 ∈ Ring) | ||
| Theorem | lnrlnm 43125 | Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
| ⊢ (𝐴 ∈ LNoeR → (ringLMod‘𝐴) ∈ LNoeM) | ||
| Theorem | islnr2 43126* | 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 43127 | 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 43128* | 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 43129 | Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
| ⊢ (𝑅 ∈ LPIR → 𝑅 ∈ LNoeR) | ||
| Theorem | lnrfrlm 43130 | Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.) |
| ⊢ 𝑌 = (𝑅 freeLMod 𝐼) ⇒ ⊢ ((𝑅 ∈ LNoeR ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM) | ||
| Theorem | lnrfg 43131 | 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 43132 | 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 43133 | The leading ideal sequence used in the Hilbert Basis Theorem. |
| class ldgIdlSeq | ||
| Definition | df-ldgis 43134* | 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 43142. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
| ⊢ ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}))) | ||
| Theorem | hbtlem1 43135* | Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) = {𝑗 ∣ ∃𝑘 ∈ 𝐼 ((𝐷‘𝑘) ≤ 𝑋 ∧ 𝑗 = ((coe1‘𝑘)‘𝑋))}) | ||
| Theorem | hbtlem2 43136 | Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝑇 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) ∈ 𝑇) | ||
| Theorem | hbtlem7 43137 | Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ 𝑇 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑆‘𝐼):ℕ0⟶𝑇) | ||
| Theorem | hbtlem4 43138 | The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) & ⊢ (𝜑 → 𝑌 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐼)‘𝑌)) | ||
| Theorem | hbtlem3 43139 | The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐼 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐽)‘𝑋)) | ||
| Theorem | hbtlem5 43140* | The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝑆 = (ldgIdlSeq‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐼 ⊆ 𝐽) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 ((𝑆‘𝐽)‘𝑥) ⊆ ((𝑆‘𝐼)‘𝑥)) ⇒ ⊢ (𝜑 → 𝐼 = 𝐽) | ||
| Theorem | hbtlem6 43141* | 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 43142 | 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 43143 | Extend class notation with the class of monic polynomials. |
| class Monic | ||
| Syntax | cplylt 43144 | Extend class notation with the class of limited-degree polynomials. |
| class Poly< | ||
| Definition | df-mnc 43145* | Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
| ⊢ Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1}) | ||
| Definition | df-plylt 43146* | Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.) |
| ⊢ Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)}) | ||
| Theorem | dgrsub2 43147 | 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 43148 | Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
| ⊢ (𝑃 ∈ ( Monic ‘𝑆) ↔ (𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1)) | ||
| Theorem | mncply 43149 | A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
| ⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ∈ (Poly‘𝑆)) | ||
| Theorem | mnccoe 43150 | A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
| ⊢ (𝑃 ∈ ( Monic ‘𝑆) → ((coeff‘𝑃)‘(deg‘𝑃)) = 1) | ||
| Theorem | mncn0 43151 | A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
| ⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑃 ≠ 0𝑝) | ||
| Syntax | cdgraa 43152 | Extend class notation to include the degree function for algebraic numbers. |
| class degAA | ||
| Syntax | cmpaa 43153 | Extend class notation to include the minimal polynomial for an algebraic number. |
| class minPolyAA | ||
| Definition | df-dgraa 43154* | 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 43155* | 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 43156* | 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 43157* | 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 43158 | Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
| ⊢ (𝐴 ∈ 𝔸 → (degAA‘𝐴) ∈ ℕ) | ||
| Theorem | dgraaf 43159 | 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 43160 | 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 43161 | 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 43162* | 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 43163* | 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 43164 | 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 43165 | Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
| ⊢ (𝐴 ∈ 𝔸 → (minPolyAA‘𝐴) ∈ (Poly‘ℚ)) | ||
| Theorem | mpaadgr 43166 | Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
| ⊢ (𝐴 ∈ 𝔸 → (deg‘(minPolyAA‘𝐴)) = (degAA‘𝐴)) | ||
| Theorem | mpaaroot 43167 | 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 43168 | Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
| ⊢ (𝐴 ∈ 𝔸 → ((coeff‘(minPolyAA‘𝐴))‘(degAA‘𝐴)) = 1) | ||
| Syntax | citgo 43169 | Extend class notation with the integral-over predicate. |
| class IntgOver | ||
| Syntax | cza 43170 | Extend class notation with the class of algebraic integers. |
| class ℤ | ||
| Definition | df-itgo 43171* | 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 43174. 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 43172 | 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 43173* | Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| ⊢ (𝑆 ⊆ ℂ → (IntgOver‘𝑆) = {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑆)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}) | ||
| Theorem | aaitgo 43174 | The standard algebraic numbers 𝔸 are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| ⊢ 𝔸 = (IntgOver‘ℚ) | ||
| Theorem | itgoss 43175 | An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (IntgOver‘𝑆) ⊆ (IntgOver‘𝑇)) | ||
| Theorem | itgocn 43176 | All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| ⊢ (IntgOver‘𝑆) ⊆ ℂ | ||
| Theorem | cnsrexpcl 43177 | Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
| ⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑋↑𝑌) ∈ 𝑆) | ||
| Theorem | fsumcnsrcl 43178* | Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
| ⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) | ||
| Theorem | cnsrplycl 43179 | Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
| ⊢ (𝜑 → 𝑆 ∈ (SubRing‘ℂfld)) & ⊢ (𝜑 → 𝑃 ∈ (Poly‘𝐶)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝑃‘𝑋) ∈ 𝑆) | ||
| Theorem | rgspnid 43180 | The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
| ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑆 = ((RingSpan‘𝑅)‘𝐴)) ⇒ ⊢ (𝜑 → 𝑆 = 𝐴) | ||
| Theorem | rngunsnply 43181* | 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 43182* | Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
| ⊢ (𝜑 → 𝐹 = (𝑗 ∈ 𝑆 ↦ if(𝑗 = 𝐾, 1, 0))) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑆) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑖 ∈ 𝑆 ((𝐹‘𝑖) · 𝐵) = ⦋𝐾 / 𝑖⦌𝐵) | ||
| Syntax | cmend 43183 | Syntax for module endomorphism algebra. |
| class MEndo | ||
| Definition | df-mend 43184* | 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 ( ·𝑠 ‘𝑚)𝑦))〉})) | ||
| Theorem | algstr 43185 | Lemma to shorten proofs of algbase 43186 through algvsca 43190. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
| ⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ 𝐴 Struct 〈1, 6〉 | ||
| Theorem | algbase 43186 | The base set of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
| ⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐴)) | ||
| Theorem | algaddg 43187 | The additive operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
| ⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ ( + ∈ 𝑉 → + = (+g‘𝐴)) | ||
| Theorem | algmulr 43188 | The multiplicative operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
| ⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ ( × ∈ 𝑉 → × = (.r‘𝐴)) | ||
| Theorem | algsca 43189 | The set of scalars of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
| ⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝑆 = (Scalar‘𝐴)) | ||
| Theorem | algvsca 43190 | The scalar product operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
| ⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ ( · ∈ 𝑉 → · = ( ·𝑠 ‘𝐴)) | ||
| Theorem | mendval 43191* | Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
| ⊢ 𝐵 = (𝑀 LMHom 𝑀) & ⊢ + = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f (+g‘𝑀)𝑦)) & ⊢ × = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ · = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦)) ⇒ ⊢ (𝑀 ∈ 𝑋 → (MEndo‘𝑀) = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉})) | ||
| Theorem | mendbas 43192 | Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
| ⊢ 𝐴 = (MEndo‘𝑀) ⇒ ⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) | ||
| Theorem | mendplusgfval 43193* | Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
| ⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (+g‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦)) | ||
| Theorem | mendplusg 43194 | A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
| ⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ + = (+g‘𝑀) & ⊢ ✚ = (+g‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌)) | ||
| Theorem | mendmulrfval 43195* | Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
| ⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (.r‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) | ||
| Theorem | mendmulr 43196 | A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
| ⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = (.r‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∘ 𝑌)) | ||
| Theorem | mendsca 43197 | The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
| ⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ 𝑆 = (Scalar‘𝐴) | ||
| Theorem | mendvscafval 43198* | Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
| ⊢ 𝐴 = (MEndo‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐸 = (Base‘𝑀) ⇒ ⊢ ( ·𝑠 ‘𝐴) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦)) | ||
| Theorem | mendvsca 43199 | A specific scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
| ⊢ 𝐴 = (MEndo‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐸 = (Base‘𝑀) & ⊢ ∙ = ( ·𝑠 ‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∙ 𝑌) = ((𝐸 × {𝑋}) ∘f · 𝑌)) | ||
| Theorem | mendring 43200 | The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
| ⊢ 𝐴 = (MEndo‘𝑀) ⇒ ⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |