P. 336 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33501-33600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	0ringidl 33501	The zero ideal is the only ideal of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → (LIdeal‘𝑅) = {{ 0 }})
Theorem	pidlnzb 33502	A principal ideal is nonzero iff it is generated by a nonzero elements (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 ≠ 0 ↔ (𝐾‘{𝑋}) ≠ { 0 }))
Theorem	lidlunitel 33503	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 33504	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 33505*	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 33506*	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 33507	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 33508*	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 33509*	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 33510	Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024.)
⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑈) → (𝐼 ∩ 𝐽) ∈ 𝑈)
Theorem	idlinsubrg 33511	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 33512	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 33513	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 33514	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))
21.3.10.40  Prime Ideals
Syntax	cprmidl 33515	Extend class notation with the class of prime ideals.
class PrmIdeal
Definition	df-prmidl 33516*	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 33521 and isprmidlc 33527. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 14-Jan-2024.)
⊢ PrmIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})
Theorem	prmidlval 33517*	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 33518*	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 33519	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 33520*	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 33521*	A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 38402 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 33522	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 33523	A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ¬ 1 ∈ 𝐼)
Theorem	prmidlidl 33524	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 33525	Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024.)
⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) ⊆ (LIdeal‘𝑅))
Theorem	cringm4 33526	Commutative/associative law for commutative ring. (Contributed by Thierry Arnoux, 14-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 · 𝑌) · (𝑍 · 𝑊)) = ((𝑋 · 𝑍) · (𝑌 · 𝑊)))
Theorem	isprmidlc 33527*	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 33528	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 33529	The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → (PrmIdeal‘𝑅) = ∅)
Theorem	prmidl0 33530	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 33531	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 33532	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 33533	A quotient by a prime ideal is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.)
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼))    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ IDomn)
Theorem	qsidom 33534	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 33535	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 33536*	Lemma for ssdifidl 33537: The set 𝑃 used in the proof of ssdifidl 33537 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)    &   ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}    &   ⊢ (𝜑 → 𝑍 ⊆ 𝑃)    &   ⊢ (𝜑 → 𝑍 ≠ ∅)    &   ⊢ (𝜑 → [⊊] Or 𝑍)    ⇒   ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃)
Theorem	ssdifidl 33537*	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 33538*	If the set 𝑆 of ssdifidl 33537 is multiplicatively closed, then the ideal 𝑖 is prime. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀))    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)    &   ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}    ⇒   ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗))
21.3.10.41  Maximal Ideals
Syntax	cmxidl 33539	Extend class notation with the class of maximal ideals.
class MaxIdeal
Definition	df-mxidl 33540*	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 33541*	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 33542*	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 33543	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 33544	A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ≠ 𝐵)
Theorem	mxidlmax 33545	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 33546	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 33547	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 33548	An ideal 𝐼 strictly containing a maximal ideal 𝑀 is the whole ring 𝐵. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑀 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐼 ∖ 𝑀))    ⇒   ⊢ (𝜑 → 𝐼 = 𝐵)
Theorem	crngmxidl 33549	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 33550	Every maximal ideal is prime. Statement in [Lang] p. 92. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ × = (LSSum‘(mulGrp‘𝑅))    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (PrmIdeal‘𝑅))
Theorem	mxidlirredi 33551	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 33552	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 33553*	The set 𝑃 used in the proof of ssmxidl 33554 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝)}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝑃)    &   ⊢ (𝜑 → 𝑍 ≠ ∅)    &   ⊢ (𝜑 → [⊊] Or 𝑍)    ⇒   ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃)
Theorem	ssmxidl 33554*	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 33555	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 33556	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 33557	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 33558	If a ring's only maximal ideal is the zero ideal, it is a division ring. See also drngmxidl 33557. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑀 = (MaxIdeal‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 = {{ 0 }})    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	krull 33559*	Krull's theorem: Any nonzero ring has at least one maximal ideal. (Contributed by Thierry Arnoux, 10-Apr-2024.)
⊢ (𝑅 ∈ NzRing → ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅))
Theorem	mxidlnzrb 33560*	A ring is nonzero if and only if it has maximal ideals. (Contributed by Thierry Arnoux, 10-Apr-2024.)
⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅)))
Theorem	krullndrng 33561*	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 33562	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 33563	Group coset equivalence relation for the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐵) → (𝑅 ~QG 𝐼) = (𝑂 ~QG 𝐼))
Theorem	opprnsg 33564	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 33565	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 33566	Two sided ideal of the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (2Ideal‘𝑅) = (2Ideal‘𝑂))
Theorem	opprmxidlabs 33567	The maximal ideal of the opposite ring's opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅))    ⇒   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘(oppr‘𝑂)))
Theorem	opprqusbas 33568	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 33569	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 33570	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 33571	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 33572	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 33573	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 33574*	Lemma for qsdrngi 33575. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑂))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑅))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ (Base‘𝑄)(𝑣(.r‘𝑄)[𝑋](𝑅 ~QG 𝑀)) = (1r‘𝑄))
Theorem	qsdrngi 33575	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 33576	Lemma for qsdrng 33577. (Contributed by Thierry Arnoux, 13-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ DivRing)    &   ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑀 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐽 ∖ 𝑀))    ⇒   ⊢ (𝜑 → 𝐽 = 𝐵)
Theorem	qsdrng 33577	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 33578	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 33579	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‘𝑅))
21.3.10.42  The semiring of ideals of a ring
Syntax	cidlsrg 33580	Extend class notation with the semiring of ideals of a ring.
class IDLsrg
Definition	df-idlsrg 33581*	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 33582	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 33583*	Lemma for idlsrgbas 33584 through idlsrgtset 33588. (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 33584	Base of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝐼 = (Base‘𝑆))
Theorem	idlsrgplusg 33585	Additive operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ ⊕ = (LSSum‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → ⊕ = (+g‘𝑆))
Theorem	idlsrg0g 33586	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 33587*	Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐵 = (LIdeal‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ⊗ = (LSSum‘𝐺)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) = (.r‘𝑆))
Theorem	idlsrgtset 33588*	Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝐽 = (TopSet‘𝑆))
Theorem	idlsrgmulrval 33589	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 33590	Ideals of a ring 𝑅 are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐵 = (LIdeal‘𝑅)    &   ⊢ ⊗ = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ∈ 𝐵)
Theorem	idlsrgmulrss1 33591	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 33592	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 33593	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 33594	The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑆 ∈ Mnd)
Theorem	idlsrgcmnd 33595	The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑆 ∈ CMnd)
21.3.10.43  Prime Elements
Theorem	rprmval 33596*	The prime elements of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (RPrime‘𝑅) = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))})
Theorem	isrprm 33597*	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 33598	A ring prime is an element of the base set. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	rprmdvds 33599	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 33600	A ring prime is nonzero. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝑄 ≠ 0 )