HomeTheorem List (p. 335 of 498)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 335 of 498) | < 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-30854) |
Hilbert Space Explorer
(30855-32377) |
Users' Mathboxes
(32378-49798) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | lidlunitel 33401 | If an ideal 𝐼 contains a unit 𝐽, then it is the whole ring. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → 𝐼 = 𝐵) | ||
| Theorem | unitpidl1 33402 | The ideal 𝐼 generated by an element 𝑋 of an integral domain 𝑅 is the unit ideal 𝐵 iff 𝑋 is a ring unit. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐼 = (𝐾‘{𝑋}) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → (𝐼 = 𝐵 ↔ 𝑋 ∈ 𝑈)) | ||
| Theorem | rhmquskerlem 33403* | The mapping 𝐽 induced by a ring homomorphism 𝐹 from the quotient group 𝑄 over 𝐹's kernel 𝐾 is a ring homomorphism. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) & ⊢ (𝜑 → 𝐺 ∈ CRing) ⇒ ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐻)) | ||
| Theorem | rhmqusker 33404* | A surjective ring homomorphism 𝐹 from 𝐺 to 𝐻 induces an isomorphism 𝐽 from 𝑄 to 𝐻, where 𝑄 is the factor group of 𝐺 by 𝐹's kernel 𝐾. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻)) & ⊢ (𝜑 → 𝐺 ∈ CRing) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) ⇒ ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingIso 𝐻)) | ||
| Theorem | ricqusker 33405 | The image 𝐻 of a ring homomorphism 𝐹 is isomorphic with the quotient ring 𝑄 over 𝐹's kernel 𝐾. This a part of what is sometimes called the first isomorphism theorem for rings. (Contributed by Thierry Arnoux, 10-Mar-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻)) & ⊢ (𝜑 → 𝐺 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑄 ≃𝑟 𝐻) | ||
| Theorem | elrspunidl 33406* | Elementhood in the span of a union of ideals. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
| ⊢ 𝑁 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑆 ⊆ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘∪ 𝑆) ↔ ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘))) | ||
| Theorem | elrspunsn 33407* | Membership to the span of an ideal 𝑅 and a single element 𝑋. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑁 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ + = (+g‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝐼)) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝑁‘(𝐼 ∪ {𝑋})) ↔ ∃𝑟 ∈ 𝐵 ∃𝑖 ∈ 𝐼 𝐴 = ((𝑟 · 𝑋) + 𝑖))) | ||
| Theorem | lidlincl 33408 | Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024.) |
| ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑈) → (𝐼 ∩ 𝐽) ∈ 𝑈) | ||
| Theorem | idlinsubrg 33409 | The intersection between an ideal and a subring is an ideal of the subring. (Contributed by Thierry Arnoux, 6-Jul-2024.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝑉 = (LIdeal‘𝑆) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) → (𝐼 ∩ 𝐴) ∈ 𝑉) | ||
| Theorem | rhmimaidl 33410 | The image of an ideal 𝐼 by a surjective ring homomorphism 𝐹 is an ideal. (Contributed by Thierry Arnoux, 6-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑇 = (LIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵 ∧ 𝐼 ∈ 𝑇) → (𝐹 “ 𝐼) ∈ 𝑈) | ||
| Theorem | drngidl 33411 | A nonzero ring is a division ring if and only if its only left ideals are the zero ideal and the unit ideal. (Proposed by Gerard Lang, 13-Mar-2025.) (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → (𝑅 ∈ DivRing ↔ 𝑈 = {{ 0 }, 𝐵})) | ||
| Theorem | drngidlhash 33412 | A ring is a division ring if and only if it admits exactly two ideals. (Proposed by Gerard Lang, 13-Mar-2025.) (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑅 ∈ DivRing ↔ (♯‘𝑈) = 2)) | ||
| Syntax | cprmidl 33413 | Extend class notation with the class of prime ideals. |
| class PrmIdeal | ||
| Definition | df-prmidl 33414* | Define the class of prime ideals of a ring 𝑅. A proper ideal 𝐼 of 𝑅 is prime if whenever 𝐴𝐵 ⊆ 𝐼 for ideals 𝐴 and 𝐵, either 𝐴 ⊆ 𝐼 or 𝐵 ⊆ 𝐼. The more familiar definition using elements rather than ideals is equivalent provided 𝑅 is commutative; see prmidl2 33419 and isprmidlc 33425. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 14-Jan-2024.) |
| ⊢ PrmIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
| Theorem | prmidlval 33415* | The class of prime ideals of a ring 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) = {𝑖 ∈ (LIdeal‘𝑅) ∣ (𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥 · 𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
| Theorem | isprmidl 33416* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑃 ∈ (PrmIdeal‘𝑅) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃))))) | ||
| Theorem | prmidlnr 33417 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ≠ 𝐵) | ||
| Theorem | prmidl 33418* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅))) ∧ ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐽 (𝑥 · 𝑦) ∈ 𝑃) → (𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃)) | ||
| Theorem | prmidl2 33419* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 38071 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑃 ∈ (LIdeal‘𝑅)) ∧ (𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃)))) → 𝑃 ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | idlmulssprm 33420 | Let 𝑃 be a prime ideal containing the product (𝐼 × 𝐽) of two ideals 𝐼 and 𝐽. Then 𝐼 ⊆ 𝑃 or 𝐽 ⊆ 𝑃. (Contributed by Thierry Arnoux, 13-Apr-2024.) |
| ⊢ × = (LSSum‘(mulGrp‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑃 ∈ (PrmIdeal‘𝑅)) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → (𝐼 × 𝐽) ⊆ 𝑃) ⇒ ⊢ (𝜑 → (𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃)) | ||
| Theorem | pridln1 33421 | A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ¬ 1 ∈ 𝐼) | ||
| Theorem | prmidlidl 33422 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ∈ (LIdeal‘𝑅)) | ||
| Theorem | prmidlssidl 33423 | Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) ⊆ (LIdeal‘𝑅)) | ||
| Theorem | cringm4 33424 | Commutative/associative law for commutative ring. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 · 𝑌) · (𝑍 · 𝑊)) = ((𝑋 · 𝑍) · (𝑌 · 𝑊))) | ||
| Theorem | isprmidlc 33425* | The predicate "is prime ideal" for commutative rings. Alternate definition for commutative rings. See definition in [Lang] p. 92. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → (𝑃 ∈ (PrmIdeal‘𝑅) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))))) | ||
| Theorem | prmidlc 33426 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ (𝐼 · 𝐽) ∈ 𝑃)) → (𝐼 ∈ 𝑃 ∨ 𝐽 ∈ 𝑃)) | ||
| Theorem | 0ringprmidl 33427 | The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → (PrmIdeal‘𝑅) = ∅) | ||
| Theorem | prmidl0 33428 | The zero ideal of a commutative ring 𝑅 is a prime ideal if and only if 𝑅 is an integral domain. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
| ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ { 0 } ∈ (PrmIdeal‘𝑅)) ↔ 𝑅 ∈ IDomn) | ||
| Theorem | rhmpreimaprmidl 33429 | The preimage of a prime ideal by a ring homomorphism is a prime ideal. (Contributed by Thierry Arnoux, 29-Jun-2024.) |
| ⊢ 𝑃 = (PrmIdeal‘𝑅) ⇒ ⊢ (((𝑆 ∈ CRing ∧ 𝐹 ∈ (𝑅 RingHom 𝑆)) ∧ 𝐽 ∈ (PrmIdeal‘𝑆)) → (◡𝐹 “ 𝐽) ∈ 𝑃) | ||
| Theorem | qsidomlem1 33430 | If the quotient ring of a commutative ring relative to an ideal is an integral domain, that ideal must be prime. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) → 𝐼 ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | qsidomlem2 33431 | A quotient by a prime ideal is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ IDomn) | ||
| Theorem | qsidom 33432 | An ideal 𝐼 in the commutative ring 𝑅 is prime if and only if the factor ring 𝑄 is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (𝑄 ∈ IDomn ↔ 𝐼 ∈ (PrmIdeal‘𝑅))) | ||
| Theorem | qsnzr 33433 | A quotient of a non-zero ring by a proper ideal is a non-zero ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ (𝜑 → 𝐼 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝑄 ∈ NzRing) | ||
| Theorem | ssdifidllem 33434* | Lemma for ssdifidl 33435: The set 𝑃 used in the proof of ssdifidl 33435 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅) & ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)} & ⊢ (𝜑 → 𝑍 ⊆ 𝑃) & ⊢ (𝜑 → 𝑍 ≠ ∅) & ⊢ (𝜑 → [⊊] Or 𝑍) ⇒ ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃) | ||
| Theorem | ssdifidl 33435* | Let 𝑅 be a ring, and let 𝐼 be an ideal of 𝑅 disjoint with a set 𝑆. Then there exists an ideal 𝑖, maximal among the set 𝑃 of ideals containing 𝐼 and disjoint with 𝑆. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅) & ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)} ⇒ ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) | ||
| Theorem | ssdifidlprm 33436* | If the set 𝑆 of ssdifidl 33435 is multiplicatively closed, then the ideal 𝑖 is prime. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀)) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅) & ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)} ⇒ ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) | ||
| Syntax | cmxidl 33437 | Extend class notation with the class of maximal ideals. |
| class MaxIdeal | ||
| Definition | df-mxidl 33438* | Define the class of maximal ideals of a ring 𝑅. A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ MaxIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑗 ∈ (LIdeal‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = (Base‘𝑟))))}) | ||
| Theorem | mxidlval 33439* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (MaxIdeal‘𝑅) = {𝑖 ∈ (LIdeal‘𝑅) ∣ (𝑖 ≠ 𝐵 ∧ ∀𝑗 ∈ (LIdeal‘𝑅)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = 𝐵)))}) | ||
| Theorem | ismxidl 33440* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ (𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵 ∧ ∀𝑗 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑗 → (𝑗 = 𝑀 ∨ 𝑗 = 𝐵))))) | ||
| Theorem | mxidlidl 33441 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (LIdeal‘𝑅)) | ||
| Theorem | mxidlnr 33442 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ≠ 𝐵) | ||
| Theorem | mxidlmax 33443 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝑀 ⊆ 𝐼)) → (𝐼 = 𝑀 ∨ 𝐼 = 𝐵)) | ||
| Theorem | mxidln1 33444 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → ¬ 1 ∈ 𝑀) | ||
| Theorem | mxidlnzr 33445 | A ring with a maximal ideal is a nonzero ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑅 ∈ NzRing) | ||
| Theorem | mxidlmaxv 33446 | An ideal 𝐼 strictly containing a maximal ideal 𝑀 is the whole ring 𝐵. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑀 ⊆ 𝐼) & ⊢ (𝜑 → 𝑋 ∈ (𝐼 ∖ 𝑀)) ⇒ ⊢ (𝜑 → 𝐼 = 𝐵) | ||
| Theorem | crngmxidl 33447 | In a commutative ring, maximal ideals of the opposite ring coincide with maximal ideals. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑀 = (MaxIdeal‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝑀 = (MaxIdeal‘𝑂)) | ||
| Theorem | mxidlprm 33448 | Every maximal ideal is prime. Statement in [Lang] p. 92. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ × = (LSSum‘(mulGrp‘𝑅)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | mxidlirredi 33449 | In an integral domain, the generator of a maximal ideal is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑀 = (𝐾‘{𝑋}) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) ⇒ ⊢ (𝜑 → 𝑋 ∈ (Irred‘𝑅)) | ||
| Theorem | mxidlirred 33450 | In a principal ideal domain, maximal ideals are exactly the ideals generated by irreducible elements. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑀 = (𝐾‘{𝑋}) & ⊢ (𝜑 → 𝑅 ∈ PID) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑀 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ 𝑋 ∈ (Irred‘𝑅))) | ||
| Theorem | ssmxidllem 33451* | The set 𝑃 used in the proof of ssmxidl 33452 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝)} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐼 ≠ 𝐵) & ⊢ (𝜑 → 𝑍 ⊆ 𝑃) & ⊢ (𝜑 → 𝑍 ≠ ∅) & ⊢ (𝜑 → [⊊] Or 𝑍) ⇒ ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃) | ||
| Theorem | ssmxidl 33452* | Let 𝑅 be a ring, and let 𝐼 be a proper ideal of 𝑅. Then there is a maximal ideal of 𝑅 containing 𝐼. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ∃𝑚 ∈ (MaxIdeal‘𝑅)𝐼 ⊆ 𝑚) | ||
| Theorem | drnglidl1ne0 33453 | In a nonzero ring, the zero ideal is different of the unit ideal. (Contributed by Thierry Arnoux, 16-Mar-2025.) |
| ⊢ 0 = (0g‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → 𝐵 ≠ { 0 }) | ||
| Theorem | drng0mxidl 33454 | In a division ring, the zero ideal is a maximal ideal. (Contributed by Thierry Arnoux, 16-Mar-2025.) |
| ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → { 0 } ∈ (MaxIdeal‘𝑅)) | ||
| Theorem | drngmxidl 33455 | The zero ideal is the only ideal of a division ring. (Contributed by Thierry Arnoux, 16-Mar-2025.) |
| ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → (MaxIdeal‘𝑅) = {{ 0 }}) | ||
| Theorem | drngmxidlr 33456 | If a ring's only maximal ideal is the zero ideal, it is a division ring. See also drngmxidl 33455. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑀 = (MaxIdeal‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 = {{ 0 }}) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
| Theorem | krull 33457* | Krull's theorem: Any nonzero ring has at least one maximal ideal. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
| ⊢ (𝑅 ∈ NzRing → ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅)) | ||
| Theorem | mxidlnzrb 33458* | A ring is nonzero if and only if it has maximal ideals. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
| ⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅))) | ||
| Theorem | krullndrng 33459* | Krull's theorem for non-division-rings: Existence of a nonzero maximal ideal. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ (MaxIdeal‘𝑅)𝑚 ≠ { 0 }) | ||
| Theorem | opprabs 33460 | The opposite ring of the opposite ring is the original ring. Note the conditions on this theorem, which makes it unpractical in case we only have e.g. 𝑅 ∈ Ring as a premise. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑅) & ⊢ (𝜑 → (.r‘ndx) ∈ dom 𝑅) & ⊢ (𝜑 → · Fn (𝐵 × 𝐵)) ⇒ ⊢ (𝜑 → 𝑅 = (oppr‘𝑂)) | ||
| Theorem | oppreqg 33461 | Group coset equivalence relation for the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐵) → (𝑅 ~QG 𝐼) = (𝑂 ~QG 𝐼)) | ||
| Theorem | opprnsg 33462 | Normal subgroups of the opposite ring are the same as the original normal subgroups. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (NrmSGrp‘𝑅) = (NrmSGrp‘𝑂) | ||
| Theorem | opprlidlabs 33463 | The ideals of the opposite ring's opposite ring are the ideals of the original ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (LIdeal‘𝑅) = (LIdeal‘(oppr‘𝑂))) | ||
| Theorem | oppr2idl 33464 | Two sided ideal of the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (2Ideal‘𝑅) = (2Ideal‘𝑂)) | ||
| Theorem | opprmxidlabs 33465 | The maximal ideal of the opposite ring's opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) ⇒ ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘(oppr‘𝑂))) | ||
| Theorem | opprqusbas 33466 | The base of the quotient of the opposite ring is the same as the base of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (Base‘(oppr‘𝑄)) = (Base‘(𝑂 /s (𝑂 ~QG 𝐼)))) | ||
| Theorem | opprqusplusg 33467 | The group operation of the quotient of the opposite ring is the same as the group operation of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) & ⊢ 𝐸 = (Base‘𝑄) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) ⇒ ⊢ (𝜑 → (𝑋(+g‘(oppr‘𝑄))𝑌) = (𝑋(+g‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌)) | ||
| Theorem | opprqus0g 33468 | The group identity element of the quotient of the opposite ring is the same as the group identity element of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) ⇒ ⊢ (𝜑 → (0g‘(oppr‘𝑄)) = (0g‘(𝑂 /s (𝑂 ~QG 𝐼)))) | ||
| Theorem | opprqusmulr 33469 | The multiplication operation of the quotient of the opposite ring is the same as the multiplication operation of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ 𝐸 = (Base‘𝑄) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) ⇒ ⊢ (𝜑 → (𝑋(.r‘(oppr‘𝑄))𝑌) = (𝑋(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑌)) | ||
| Theorem | opprqus1r 33470 | The ring unity of the quotient of the opposite ring is the same as the ring unity of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) ⇒ ⊢ (𝜑 → (1r‘(oppr‘𝑄)) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼)))) | ||
| Theorem | opprqusdrng 33471 | The quotient of the opposite ring is a division ring iff the opposite of the quotient ring is. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) ⇒ ⊢ (𝜑 → ((oppr‘𝑄) ∈ DivRing ↔ (𝑂 /s (𝑂 ~QG 𝐼)) ∈ DivRing)) | ||
| Theorem | qsdrngilem 33472* | Lemma for qsdrngi 33473. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑂)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑅)) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ (Base‘𝑄)(𝑣(.r‘𝑄)[𝑋](𝑅 ~QG 𝑀)) = (1r‘𝑄)) | ||
| Theorem | qsdrngi 33473 | A quotient by a maximal left and maximal right ideal is a division ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑂)) ⇒ ⊢ (𝜑 → 𝑄 ∈ DivRing) | ||
| Theorem | qsdrnglem2 33474 | Lemma for qsdrng 33475. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ (2Ideal‘𝑅)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑄 ∈ DivRing) & ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑀 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 ∈ (𝐽 ∖ 𝑀)) ⇒ ⊢ (𝜑 → 𝐽 = 𝐵) | ||
| Theorem | qsdrng 33475 | An ideal 𝑀 is both left and right maximal if and only if the factor ring 𝑄 is a division ring. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ (2Ideal‘𝑅)) ⇒ ⊢ (𝜑 → (𝑄 ∈ DivRing ↔ (𝑀 ∈ (MaxIdeal‘𝑅) ∧ 𝑀 ∈ (MaxIdeal‘𝑂)))) | ||
| Theorem | qsfld 33476 | An ideal 𝑀 in the commutative ring 𝑅 is maximal if and only if the factor ring 𝑄 is a field. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝑄 ∈ Field ↔ 𝑀 ∈ (MaxIdeal‘𝑅))) | ||
| Theorem | mxidlprmALT 33477 | Every maximal ideal is prime - alternative proof. (Contributed by Thierry Arnoux, 15-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) ⇒ ⊢ (𝜑 → 𝑀 ∈ (PrmIdeal‘𝑅)) | ||
| Syntax | cidlsrg 33478 | Extend class notation with the semiring of ideals of a ring. |
| class IDLsrg | ||
| Definition | df-idlsrg 33479* | Define a structure for the ideals of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ IDLsrg = (𝑟 ∈ V ↦ ⦋(LIdeal‘𝑟) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (LSSum‘𝑟)⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}⟩})) | ||
| Theorem | idlsrgstr 33480 | A constructed semiring of ideals is a structure. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩}) ⇒ ⊢ 𝑊 Struct ⟨1, ;10⟩ | ||
| Theorem | idlsrgval 33481* | Lemma for idlsrgbas 33482 through idlsrgtset 33486. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ ⊕ = (LSSum‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ⊗ = (LSSum‘𝐺) ⇒ ⊢ (𝑅 ∈ 𝑉 → (IDLsrg‘𝑅) = ({⟨(Base‘ndx), 𝐼⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}⟩})) | ||
| Theorem | idlsrgbas 33482 | Base of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝐼 = (Base‘𝑆)) | ||
| Theorem | idlsrgplusg 33483 | Additive operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ ⊕ = (LSSum‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → ⊕ = (+g‘𝑆)) | ||
| Theorem | idlsrg0g 33484 | The zero ideal is the additive identity of the semiring of ideals. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → { 0 } = (0g‘𝑆)) | ||
| Theorem | idlsrgmulr 33485* | Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ⊗ = (LSSum‘𝐺) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) = (.r‘𝑆)) | ||
| Theorem | idlsrgtset 33486* | Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝐽 = (TopSet‘𝑆)) | ||
| Theorem | idlsrgmulrval 33487 | Value of the ring multiplication for the ideals of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ ⊗ = (.r‘𝑆) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ · = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ⊗ 𝐽) = ((RSpan‘𝑅)‘(𝐼 · 𝐽))) | ||
| Theorem | idlsrgmulrcl 33488 | Ideals of a ring 𝑅 are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ ⊗ = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ∈ 𝐵) | ||
| Theorem | idlsrgmulrss1 33489 | In a commutative ring, the product of two ideals is a subset of the first one. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ ⊗ = (.r‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ⊆ 𝐼) | ||
| Theorem | idlsrgmulrss2 33490 | The product of two ideals is a subset of the second one. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ ⊗ = (.r‘𝑆) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ⊆ 𝐽) | ||
| Theorem | idlsrgmulrssin 33491 | In a commutative ring, the product of two ideals is a subset of their intersection. (Contributed by Thierry Arnoux, 17-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ ⊗ = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ⊆ (𝐼 ∩ 𝐽)) | ||
| Theorem | idlsrgmnd 33492 | The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑆 ∈ Mnd) | ||
| Theorem | idlsrgcmnd 33493 | The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑆 ∈ CMnd) | ||
| Theorem | rprmval 33494* | The prime elements of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → (RPrime‘𝑅) = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))}) | ||
| Theorem | isrprm 33495* | Property for 𝑃 to be a prime element in the ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑃 ∈ (RPrime‘𝑅) ↔ (𝑃 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))))) | ||
| Theorem | rprmcl 33496 | A ring prime is an element of the base set. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
| Theorem | rprmdvds 33497 | If a ring prime 𝑄 divides a product 𝑋 · 𝑌, then it divides either 𝑋 or 𝑌. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∥ (𝑋 · 𝑌)) ⇒ ⊢ (𝜑 → (𝑄 ∥ 𝑋 ∨ 𝑄 ∥ 𝑌)) | ||
| Theorem | rprmnz 33498 | A ring prime is nonzero. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝑄 ≠ 0 ) | ||
| Theorem | rprmnunit 33499 | A ring prime is not a unit. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) ⇒ ⊢ (𝜑 → ¬ 𝑄 ∈ 𝑈) | ||
| Theorem | rsprprmprmidl 33500 | In a commutative ring, ideals generated by prime elements are prime ideals. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑃 ∈ (RPrime‘𝑅)) ⇒ ⊢ (𝜑 → (𝐾‘{𝑃}) ∈ (PrmIdeal‘𝑅)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |