P. 341 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34001-34100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	grplsmid 34001	The direct sum of an element 𝑋 of a subgroup 𝐴 is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝐴) → ({𝑋} ⊕ 𝐴) = 𝐴)
21.4.10.38  The quotient map
Theorem	quslsm 34002	Express the image by the quotient map in terms of direct sum. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → [𝑋](𝐺 ~QG 𝑆) = ({𝑋} ⊕ 𝑆))
Theorem	qusbas2 34003*	Alternate definition of the group quotient set, as the set of all cosets of the form ({𝑥} ⊕ 𝑁). (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ (SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → (𝐵 / (𝐺 ~QG 𝑁)) = ran (𝑥 ∈ 𝐵 ↦ ({𝑥} ⊕ 𝑁)))
Theorem	qus0g 34004	The identity element of a quotient group. (Contributed by Thierry Arnoux, 13-Mar-2025.)
⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    ⇒   ⊢ (𝑁 ∈ (NrmSGrp‘𝐺) → (0g‘𝑄) = 𝑁)
Theorem	qusima 34005*	The image of a subgroup by the natural map from elements to their cosets. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝐺 ~QG 𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    &   ⊢ (𝜑 → 𝐻 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → (𝐸‘𝐻) = (𝐹 “ 𝐻))
Theorem	qusrn 34006*	The natural map from elements to their cosets is surjective. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑈 = (𝐵 / (𝐺 ~QG 𝑁))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝐺 ~QG 𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → ran 𝐹 = 𝑈)
Theorem	nsgqus0 34007	A normal subgroup 𝑁 is a member of all subgroups 𝐹 of the quotient group by 𝑁. In fact, it is the identity element of the quotient group. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    ⇒   ⊢ ((𝑁 ∈ (NrmSGrp‘𝐺) ∧ 𝐹 ∈ (SubGrp‘𝑄)) → 𝑁 ∈ 𝐹)
Theorem	nsgmgclem 34008*	Lemma for nsgmgc 34009. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    &   ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝑄))    ⇒   ⊢ (𝜑 → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ∈ (SubGrp‘𝐺))
Theorem	nsgmgc 34009*	There is a monotone Galois connection between the lattice of subgroups of a group 𝐺 containing a normal subgroup 𝑁 and the lattice of subgroups of the quotient group 𝐺 / 𝑁. This is sometimes called the lattice theorem. (Contributed by Thierry Arnoux, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ 𝐽 = (𝑉MGalConn𝑊)    &   ⊢ 𝑉 = (toInc‘𝑆)    &   ⊢ 𝑊 = (toInc‘𝑇)    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → 𝐸𝐽𝐹)
Theorem	nsgqusf1olem1 34010*	Lemma for nsgqusf1o 34013. (Contributed by Thierry Arnoux, 4-Aug-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ ≤ = (le‘(toInc‘𝑆))    &   ⊢ ≲ = (le‘(toInc‘𝑇))    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) → ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) ∈ 𝑇)
Theorem	nsgqusf1olem2 34011*	Lemma for nsgqusf1o 34013. (Contributed by Thierry Arnoux, 4-Aug-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ ≤ = (le‘(toInc‘𝑆))    &   ⊢ ≲ = (le‘(toInc‘𝑇))    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → ran 𝐸 = 𝑇)
Theorem	nsgqusf1olem3 34012*	Lemma for nsgqusf1o 34013. (Contributed by Thierry Arnoux, 4-Aug-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ ≤ = (le‘(toInc‘𝑆))    &   ⊢ ≲ = (le‘(toInc‘𝑇))    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → ran 𝐹 = 𝑆)
Theorem	nsgqusf1o 34013*	The canonical projection homomorphism 𝐸 defines a bijective correspondence between the set 𝑆 of subgroups of 𝐺 containing a normal subgroup 𝑁 and the subgroups of the quotient group 𝐺 / 𝑁. This theorem is sometimes called the correspondence theorem, or the fourth isomorphism theorem. (Contributed by Thierry Arnoux, 4-Aug-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ}    &   ⊢ 𝑇 = (SubGrp‘𝑄)    &   ⊢ ≤ = (le‘(toInc‘𝑆))    &   ⊢ ≲ = (le‘(toInc‘𝑇))    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))    &   ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → 𝐸:𝑆–1-1-onto→𝑇)
Theorem	lmhmqusker 34014*	A surjective module 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‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 LMHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))    &   ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    ⇒   ⊢ (𝜑 → 𝐽 ∈ (𝑄 LMIso 𝐻))
Theorem	lmicqusker 34015	The image 𝐻 of a module homomorphism 𝐹 is isomorphic with the quotient module 𝑄 over 𝐹's kernel 𝐾. This is part of what is sometimes called the first isomorphism theorem for modules. (Contributed by Thierry Arnoux, 10-Mar-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 LMHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))    &   ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻))    ⇒   ⊢ (𝜑 → 𝑄 ≃𝑚 𝐻)
21.4.10.39  Ideals
Theorem	intlidl 34016	The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 8-Jun-2024.)
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → ∩ 𝐶 ∈ (LIdeal‘𝑅))
Theorem	inlidl 34017	The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by AV, 28-Jun-2026.)
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅)) → (𝐼 ∩ 𝐽) ∈ (LIdeal‘𝑅))
Theorem	pidlnzb 34018	A principal ideal is nonzero iff it is generated by a nonzero element. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 ≠ 0 ↔ (𝐾‘{𝑋}) ≠ { 0 }))
Theorem	lidlunitel 34019	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 34020	The ideal 𝐼 generated by an element 𝑋 of a commutative ring 𝑅 is the unit ideal 𝐵 iff 𝑋 is a ring unit. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐼 = (𝐾‘{𝑋})    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝐼 = 𝐵 ↔ 𝑋 ∈ 𝑈))
Theorem	rhmquskerlem 34021*	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 34022*	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 34023	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 34024*	Elementhood in the span of a union of ideals. (Contributed by Thierry Arnoux, 30-Jun-2024.) Remove dependency on ax-reg 9589 and ax-inf2 9645. (Revised by Timothy J. O'Malley, 15-Oct-2026.)
⊢ 𝑁 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑆 ⊆ (LIdeal‘𝑅))    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘∪ 𝑆) ↔ ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘)))
Theorem	elrspunsn 34025*	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 34026	Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024.)
⊢ 𝑈 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑈) → (𝐼 ∩ 𝐽) ∈ 𝑈)
Theorem	idlinsubrg 34027	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 34028	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	drngidlhash 34029	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.4.10.40  Maximal Ideals
Syntax	cmxidl 34030	Extend class notation with the class of maximal ideals.
class MaxIdeal
Definition	df-mxidl 34031*	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 34032*	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 34033*	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 34034	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 34035	A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ≠ 𝐵)
Theorem	mxidlmax 34036	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 34037	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 34038	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 34039	An ideal 𝐼 strictly containing a maximal ideal 𝑀 is the whole ring 𝐵. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑀 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐼 ∖ 𝑀))    ⇒   ⊢ (𝜑 → 𝐼 = 𝐵)
Theorem	crngmxidl 34040	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 34041	Every maximal ideal is prime. Statement in [Lang] p. 92. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ × = (LSSum‘(mulGrp‘𝑅))    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (PrmIdeal‘𝑅))
Theorem	mxidlirredi 34042	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 34043	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 34044*	The set 𝑃 used in the proof of ssmxidl 34045 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝)}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝑃)    &   ⊢ (𝜑 → 𝑍 ≠ ∅)    &   ⊢ (𝜑 → [⊊] Or 𝑍)    ⇒   ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃)
Theorem	ssmxidl 34045*	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	drng0mxidl 34046	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 34047	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 34048	If a ring's only maximal ideal is the zero ideal, it is a division ring. See also drngmxidl 34047. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑀 = (MaxIdeal‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 = {{ 0 }})    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	krull 34049*	Krull's theorem: Any nonzero ring has at least one maximal ideal. (Contributed by Thierry Arnoux, 10-Apr-2024.)
⊢ (𝑅 ∈ NzRing → ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅))
Theorem	mxidlnzrb 34050*	A ring is nonzero if and only if it has maximal ideals. (Contributed by Thierry Arnoux, 10-Apr-2024.)
⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅)))
Theorem	krullndrng 34051*	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 34052	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 34053	Group coset equivalence relation for the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐵) → (𝑅 ~QG 𝐼) = (𝑂 ~QG 𝐼))
Theorem	opprnsg 34054	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 34055	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 34056	Two sided ideal of the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (2Ideal‘𝑅) = (2Ideal‘𝑂))
Theorem	opprmxidlabs 34057	The maximal ideal of the opposite ring's opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅))    ⇒   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘(oppr‘𝑂)))
Theorem	opprqusbas 34058	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 34059	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 34060	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 34061	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 34062	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 34063	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 34064*	Lemma for qsdrngi 34065. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑂))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑅))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ (Base‘𝑄)(𝑣(.r‘𝑄)[𝑋](𝑅 ~QG 𝑀)) = (1r‘𝑄))
Theorem	qsdrngi 34065	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 34066	Lemma for qsdrng 34067. (Contributed by Thierry Arnoux, 13-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ DivRing)    &   ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑀 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐽 ∖ 𝑀))    ⇒   ⊢ (𝜑 → 𝐽 = 𝐵)
Theorem	qsdrng 34067	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 34068	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 34069	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.4.10.41  Local rings
Theorem	drnglring 34070	A division ring is a local ring. (Contributed by Thierry Arnoux, 2-Jun-2026.)
⊢ (𝜑 → 𝐹 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝐹 ∈ LRing)
Theorem	dflring2 34071*	Alternate definition of a local ring. (Contributed by Thierry Arnoux, 2-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ − = (-g‘𝑅)    ⇒   ⊢ (𝑅 ∈ LRing ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥) ∈ 𝑈)))
Theorem	dflringlem 34072	Lemma for dflring3 34075. If a ring 𝑅 has a single maximal ideal 𝑀, then any element 𝑋 outside of 𝑀 is a unit. (Contributed by Thierry Arnoux, 2-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅))    &   ⊢ (𝜑 → (MaxIdeal‘𝑅) = {𝑀})    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑀))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑈)
Theorem	dflringlem2 34073	Lemma for dflring3 34075. In a commutative local ring 𝑅, the set (𝐵 ∖ 𝑈) of non-units is an ideal. (Contributed by Thierry Arnoux, 2-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ LRing)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑈) ∈ (LIdeal‘𝑅))
Theorem	dflringlem3 34074	Lemma for dflring3 34075. In a commutative local ring 𝑅, the set (𝐵 ∖ 𝑈) of non-units is a maximal ideal. (Contributed by Thierry Arnoux, 2-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ LRing)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑈) ∈ (MaxIdeal‘𝑅))
Theorem	dflring3 34075	Alternate definition of a local ring: local rings have a single maximal ideal. (Contributed by Thierry Arnoux, 2-Jun-2026.)
⊢ (𝑅 ∈ CRing → (𝑅 ∈ LRing ↔ (MaxIdeal‘𝑅) ≈ 1o))
Theorem	dflring4 34076	Alternate definition of a local ring: the set (𝐵 ∖ 𝑈) of non-units is an ideal. (Contributed by Thierry Arnoux, 2-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → (𝑅 ∈ LRing ↔ (𝐵 ∖ 𝑈) ∈ (LIdeal‘𝑅)))
Theorem	fldlring 34077	A field is a local ring. (Contributed by Thierry Arnoux, 3-Jun-2026.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐹 ∈ Field)    ⇒   ⊢ (𝜑 → 𝐹 ∈ LRing)
21.4.10.42  The semiring of ideals of a ring
Syntax	cidlsrg 34078	Extend class notation with the semiring of ideals of a ring.
class IDLsrg
Definition	df-idlsrg 34079*	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 34080	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 34081*	Lemma for idlsrgbas 34082 through idlsrgtset 34086. (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 34082	Base of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝐼 = (Base‘𝑆))
Theorem	idlsrgplusg 34083	Additive operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ ⊕ = (LSSum‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → ⊕ = (+g‘𝑆))
Theorem	idlsrg0g 34084	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 34085*	Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐵 = (LIdeal‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ⊗ = (LSSum‘𝐺)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) = (.r‘𝑆))
Theorem	idlsrgtset 34086*	Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝐽 = (TopSet‘𝑆))
Theorem	idlsrgmulrval 34087	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 34088	Ideals of a ring 𝑅 are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐵 = (LIdeal‘𝑅)    &   ⊢ ⊗ = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ∈ 𝐵)
Theorem	idlsrgmulrss1 34089	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 34090	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 34091	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 34092	The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑆 ∈ Mnd)
Theorem	idlsrgcmnd 34093	The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑆 ∈ CMnd)
21.4.10.43  Prime Elements
Theorem	rprmval 34094*	The prime elements of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (RPrime‘𝑅) = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))})
Theorem	isrprm 34095*	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 34096	A ring prime is an element of the base set. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	rprmdvds 34097	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 34098	A ring prime is nonzero. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝑄 ≠ 0 )
Theorem	rprmnunit 34099	A ring prime is not a unit. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ¬ 𝑄 ∈ 𝑈)
Theorem	rsprprmprmidl 34100	In a commutative ring, ideals generated by prime elements are prime ideals. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑃 ∈ (RPrime‘𝑅))    ⇒   ⊢ (𝜑 → (𝐾‘{𝑃}) ∈ (PrmIdeal‘𝑅))