HomeTheorem List (p. 336 of 503)
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. 336 of 503) | < 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-30989) |
Hilbert Space Explorer
(30990-32512) |
Users' Mathboxes
(32513-50274) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | prmidl2 33501* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 38391 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 33502 | 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 33503 | A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ¬ 1 ∈ 𝐼) | ||
| Theorem | prmidlidl 33504 | 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 33505 | Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) ⊆ (LIdeal‘𝑅)) | ||
| Theorem | cringm4 33506 | Commutative/associative law for commutative ring. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 · 𝑌) · (𝑍 · 𝑊)) = ((𝑋 · 𝑍) · (𝑌 · 𝑊))) | ||
| Theorem | isprmidlc 33507* | 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 33508 | 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 33509 | The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → (PrmIdeal‘𝑅) = ∅) | ||
| Theorem | prmidl0 33510 | 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 33511 | 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 33512 | 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 33513 | A quotient by a prime ideal is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ IDomn) | ||
| Theorem | qsidom 33514 | 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 33515 | A quotient of a nonzero ring by a proper ideal is a nonzero ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ (𝜑 → 𝐼 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝑄 ∈ NzRing) | ||
| Theorem | ssdifidllem 33516* | Lemma for ssdifidl 33517: The set 𝑃 used in the proof of ssdifidl 33517 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅) & ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)} & ⊢ (𝜑 → 𝑍 ⊆ 𝑃) & ⊢ (𝜑 → 𝑍 ≠ ∅) & ⊢ (𝜑 → [⊊] Or 𝑍) ⇒ ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃) | ||
| Theorem | ssdifidl 33517* | 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 33518* | If the set 𝑆 of ssdifidl 33517 is multiplicatively closed, then the ideal 𝑖 is prime. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀)) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅) & ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)} ⇒ ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) | ||
| Syntax | cmxidl 33519 | Extend class notation with the class of maximal ideals. |
| class MaxIdeal | ||
| Definition | df-mxidl 33520* | 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 33521* | 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 33522* | 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 33523 | 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 33524 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ≠ 𝐵) | ||
| Theorem | mxidlmax 33525 | 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 33526 | 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 33527 | 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 33528 | An ideal 𝐼 strictly containing a maximal ideal 𝑀 is the whole ring 𝐵. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑀 ⊆ 𝐼) & ⊢ (𝜑 → 𝑋 ∈ (𝐼 ∖ 𝑀)) ⇒ ⊢ (𝜑 → 𝐼 = 𝐵) | ||
| Theorem | crngmxidl 33529 | 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 33530 | Every maximal ideal is prime. Statement in [Lang] p. 92. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ × = (LSSum‘(mulGrp‘𝑅)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | mxidlirredi 33531 | 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 33532 | 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 33533* | The set 𝑃 used in the proof of ssmxidl 33534 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝)} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐼 ≠ 𝐵) & ⊢ (𝜑 → 𝑍 ⊆ 𝑃) & ⊢ (𝜑 → 𝑍 ≠ ∅) & ⊢ (𝜑 → [⊊] Or 𝑍) ⇒ ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃) | ||
| Theorem | ssmxidl 33534* | 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 33535 | 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 33536 | 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 33537 | 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 33538 | If a ring's only maximal ideal is the zero ideal, it is a division ring. See also drngmxidl 33537. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑀 = (MaxIdeal‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 = {{ 0 }}) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
| Theorem | krull 33539* | Krull's theorem: Any nonzero ring has at least one maximal ideal. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
| ⊢ (𝑅 ∈ NzRing → ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅)) | ||
| Theorem | mxidlnzrb 33540* | A ring is nonzero if and only if it has maximal ideals. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
| ⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅))) | ||
| Theorem | krullndrng 33541* | 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 33542 | 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 33543 | Group coset equivalence relation for the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐵) → (𝑅 ~QG 𝐼) = (𝑂 ~QG 𝐼)) | ||
| Theorem | opprnsg 33544 | 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 33545 | 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 33546 | Two sided ideal of the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (2Ideal‘𝑅) = (2Ideal‘𝑂)) | ||
| Theorem | opprmxidlabs 33547 | The maximal ideal of the opposite ring's opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) ⇒ ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘(oppr‘𝑂))) | ||
| Theorem | opprqusbas 33548 | 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 33549 | 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 33550 | 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 33551 | 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 33552 | 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 33553 | 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 33554* | Lemma for qsdrngi 33555. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑂)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑅)) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ (Base‘𝑄)(𝑣(.r‘𝑄)[𝑋](𝑅 ~QG 𝑀)) = (1r‘𝑄)) | ||
| Theorem | qsdrngi 33555 | 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 33556 | Lemma for qsdrng 33557. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) & ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑀 ∈ (2Ideal‘𝑅)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑄 ∈ DivRing) & ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑀 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 ∈ (𝐽 ∖ 𝑀)) ⇒ ⊢ (𝜑 → 𝐽 = 𝐵) | ||
| Theorem | qsdrng 33557 | 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 33558 | 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 33559 | 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 33560 | Extend class notation with the semiring of ideals of a ring. |
| class IDLsrg | ||
| Definition | df-idlsrg 33561* | 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 33562 | 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 33563* | Lemma for idlsrgbas 33564 through idlsrgtset 33568. (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 33564 | Base of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝐼 = (Base‘𝑆)) | ||
| Theorem | idlsrgplusg 33565 | Additive operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ ⊕ = (LSSum‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → ⊕ = (+g‘𝑆)) | ||
| Theorem | idlsrg0g 33566 | 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 33567* | Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ⊗ = (LSSum‘𝐺) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) = (.r‘𝑆)) | ||
| Theorem | idlsrgtset 33568* | Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝐽 = (TopSet‘𝑆)) | ||
| Theorem | idlsrgmulrval 33569 | 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 33570 | Ideals of a ring 𝑅 are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) & ⊢ 𝐵 = (LIdeal‘𝑅) & ⊢ ⊗ = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ∈ 𝐵) | ||
| Theorem | idlsrgmulrss1 33571 | 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 33572 | 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 33573 | 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 33574 | The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑆 ∈ Mnd) | ||
| Theorem | idlsrgcmnd 33575 | The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑆 = (IDLsrg‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝑆 ∈ CMnd) | ||
| Theorem | rprmval 33576* | The prime elements of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → (RPrime‘𝑅) = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))}) | ||
| Theorem | isrprm 33577* | 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 33578 | A ring prime is an element of the base set. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
| Theorem | rprmdvds 33579 | 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 33580 | A ring prime is nonzero. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝑄 ≠ 0 ) | ||
| Theorem | rprmnunit 33581 | A ring prime is not a unit. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) ⇒ ⊢ (𝜑 → ¬ 𝑄 ∈ 𝑈) | ||
| Theorem | rsprprmprmidl 33582 | In a commutative ring, ideals generated by prime elements are prime ideals. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑃 ∈ (RPrime‘𝑅)) ⇒ ⊢ (𝜑 → (𝐾‘{𝑃}) ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | rsprprmprmidlb 33583 | In an integral domain, an ideal generated by a single element is a prime iff that element is prime. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 0 = (0g‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑃 ↔ (𝐾‘{𝑋}) ∈ (PrmIdeal‘𝑅))) | ||
| Theorem | rprmndvdsr1 33584 | A ring prime element does not divide the ring multiplicative identity. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 1 = (1r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) ⇒ ⊢ (𝜑 → ¬ 𝑄 ∥ 1 ) | ||
| Theorem | rprmasso 33585 | In an integral domain, the associate of a prime is a prime. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∥ 𝑌) & ⊢ (𝜑 → 𝑌 ∥ 𝑋) ⇒ ⊢ (𝜑 → 𝑌 ∈ 𝑃) | ||
| Theorem | rprmasso2 33586 | In an integral domain, if a prime element divides another, they are associates. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∥ 𝑌) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) ⇒ ⊢ (𝜑 → 𝑌 ∥ 𝑋) | ||
| Theorem | rprmasso3 33587* | In an integral domain, if a prime element divides another, they are associates. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∥ 𝑌) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ · = (.r‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ 𝑈 (𝑡 · 𝑋) = 𝑌) | ||
| Theorem | unitmulrprm 33588 | A ring unit multiplied by a ring prime is a ring prime. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) ⇒ ⊢ (𝜑 → (𝐼 · 𝑄) ∈ 𝑃) | ||
| Theorem | rprmndvdsru 33589 | A ring prime element does not divide any ring unit. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑇 ∈ 𝑈) ⇒ ⊢ (𝜑 → ¬ 𝑄 ∥ 𝑇) | ||
| Theorem | rprmirredlem 33590 | Lemma for rprmirred 33591. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑄 ≠ 0 ) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑈)) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 = (𝑋 · 𝑌)) & ⊢ (𝜑 → 𝑄 ∥ 𝑋) ⇒ ⊢ (𝜑 → 𝑌 ∈ 𝑈) | ||
| Theorem | rprmirred 33591 | In an integral domain, ring primes are irreducible. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝐼 = (Irred‘𝑅) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → 𝑄 ∈ 𝐼) | ||
| Theorem | rprmirredb 33592 | In a principal ideal domain, the converse of rprmirred 33591 holds, i.e. irreducible elements are prime. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝐼 = (Irred‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ PID) ⇒ ⊢ (𝜑 → 𝐼 = 𝑃) | ||
| Theorem | rprmdvdspow 33593 | If a prime element divides a ring "power", it divides the term. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝑀) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑄 ∥ (𝑁 ↑ 𝑋)) ⇒ ⊢ (𝜑 → 𝑄 ∥ 𝑋) | ||
| Theorem | rprmdvdsprod 33594* | If a prime element 𝑄 divides a product, then it divides one term. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 finSupp 1 ) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ (𝜑 → 𝑄 ∥ (𝑀 Σg 𝐹)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝐹 supp 1 )𝑄 ∥ (𝐹‘𝑥)) | ||
| Theorem | 1arithidomlem1 33595* | Lemma for 1arithidom 33597. (Contributed by Thierry Arnoux, 30-May-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐽 = (0..^(♯‘𝐹)) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ Word 𝑃) & ⊢ (𝜑 → 𝐺 ∈ Word 𝑃) & ⊢ (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg 𝐺)) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → ∀𝑔 ∈ Word 𝑃(∃𝑘 ∈ 𝑈 (𝑀 Σg 𝐹) = (𝑘 · (𝑀 Σg 𝑔)) → ∃𝑤∃𝑢 ∈ (𝑈 ↑m (0..^(♯‘𝐹)))(𝑤:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) ∧ 𝑔 = (𝑢 ∘f · (𝐹 ∘ 𝑤))))) & ⊢ (𝜑 → 𝐻 ∈ Word 𝑃) & ⊢ (𝜑 → ∃𝑘 ∈ 𝑈 (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑘 · (𝑀 Σg 𝐻))) & ⊢ (𝜑 → 𝐾 ∈ (0..^(♯‘𝐻))) & ⊢ (𝜑 → 𝑄(∥r‘𝑅)(𝐻‘𝐾)) & ⊢ (𝜑 → 𝑇 ∈ 𝑈) & ⊢ (𝜑 → (𝑇 · 𝑄) = (𝐻‘𝐾)) & ⊢ (𝜑 → 𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) & ⊢ (𝜑 → (𝐻 ∘ 𝑆) = (((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻‘𝐾)”⟩)) & ⊢ (𝜑 → 𝑁 ∈ 𝑈) & ⊢ (𝜑 → (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑁 · (𝑀 Σg 𝐻))) ⇒ ⊢ (𝜑 → ∃𝑐∃𝑑 ∈ (𝑈 ↑m (0..^(♯‘𝐹)))(𝑐:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) ∧ ((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) = (𝑑 ∘f · (𝐹 ∘ 𝑐)))) | ||
| Theorem | 1arithidomlem2 33596* | Lemma for 1arithidom 33597: induction step. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐽 = (0..^(♯‘𝐹)) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ Word 𝑃) & ⊢ (𝜑 → 𝐺 ∈ Word 𝑃) & ⊢ (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg 𝐺)) & ⊢ (𝜑 → 𝑄 ∈ 𝑃) & ⊢ (𝜑 → ∀𝑔 ∈ Word 𝑃(∃𝑘 ∈ 𝑈 (𝑀 Σg 𝐹) = (𝑘 · (𝑀 Σg 𝑔)) → ∃𝑤∃𝑢 ∈ (𝑈 ↑m (0..^(♯‘𝐹)))(𝑤:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) ∧ 𝑔 = (𝑢 ∘f · (𝐹 ∘ 𝑤))))) & ⊢ (𝜑 → 𝐻 ∈ Word 𝑃) & ⊢ (𝜑 → ∃𝑘 ∈ 𝑈 (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑘 · (𝑀 Σg 𝐻))) & ⊢ (𝜑 → 𝐾 ∈ (0..^(♯‘𝐻))) & ⊢ (𝜑 → 𝑄(∥r‘𝑅)(𝐻‘𝐾)) & ⊢ (𝜑 → 𝑇 ∈ 𝑈) & ⊢ (𝜑 → (𝑇 · 𝑄) = (𝐻‘𝐾)) & ⊢ (𝜑 → 𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) & ⊢ (𝜑 → (𝐻 ∘ 𝑆) = (((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) ++ ⟨“(𝐻‘𝐾)”⟩)) & ⊢ (𝜑 → 𝑁 ∈ 𝑈) & ⊢ (𝜑 → (𝑀 Σg (𝐹 ++ ⟨“𝑄”⟩)) = (𝑁 · (𝑀 Σg 𝐻))) & ⊢ (𝜑 → 𝐷 ∈ (𝑈 ↑m (0..^(♯‘𝐹)))) & ⊢ (𝜑 → 𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹))) & ⊢ (𝜑 → ((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) = (𝐷 ∘f · (𝐹 ∘ 𝐶))) ⇒ ⊢ (𝜑 → (((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ ◡𝑆):(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩)))–1-1-onto→(0..^(♯‘(𝐹 ++ ⟨“𝑄”⟩))) ∧ 𝐻 = (((𝐷 ++ ⟨“𝑇”⟩) ∘ ◡𝑆) ∘f · ((𝐹 ++ ⟨“𝑄”⟩) ∘ ((𝐶 ++ ⟨“(♯‘𝐹)”⟩) ∘ ◡𝑆))))) | ||
| Theorem | 1arithidom 33597* | Uniqueness of prime factorizations in an integral domain 𝑅. Given two equal products 𝐹 and 𝐺 of prime elements, 𝐹 and 𝐺 are equal up to a renumbering 𝑤 and a multiplication by units 𝑢. See also 1arith 16898. Chapter VII, Paragraph 3, Section 3, Proposition 2 of [BourbakiCAlg2], p. 228. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐽 = (0..^(♯‘𝐹)) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ Word 𝑃) & ⊢ (𝜑 → 𝐺 ∈ Word 𝑃) & ⊢ (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg 𝐺)) ⇒ ⊢ (𝜑 → ∃𝑤∃𝑢 ∈ (𝑈 ↑m 𝐽)(𝑤:𝐽–1-1-onto→𝐽 ∧ 𝐺 = (𝑢 ∘f · (𝐹 ∘ 𝑤)))) | ||
| Syntax | cufd 33598 | Class of unique factorization domains. |
| class UFD | ||
| Definition | df-ufd 33599* | Define the class of unique factorization domains. A unique factorization domain (UFD for short), is an integral domain such that every nonzero prime ideal contains a prime element (this is a characterization due to Irving Kaplansky). A UFD is sometimes also called a "factorial ring" following the terminology of Bourbaki. (Contributed by Mario Carneiro, 17-Feb-2015.) Exclude the 0 prime ideal. (Revised by Thierry Arnoux, 9-May-2025.) Exclude the 0 ring. (Revised by Thierry Arnoux, 14-Jun-2025.) |
| ⊢ UFD = {𝑟 ∈ IDomn ∣ ∀𝑖 ∈ ((PrmIdeal‘𝑟) ∖ {{(0g‘𝑟)}})(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅} | ||
| Theorem | isufd 33600* | The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝐼 = (PrmIdeal‘𝑅) & ⊢ 𝑃 = (RPrime‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑖 ∈ (𝐼 ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |