P. 335 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33401-33500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	qsidom 33401	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 33402	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 33403*	Lemma for ssdifidl 33404: The set 𝑃 used in the proof of ssdifidl 33404 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)    &   ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}    &   ⊢ (𝜑 → 𝑍 ⊆ 𝑃)    &   ⊢ (𝜑 → 𝑍 ≠ ∅)    &   ⊢ (𝜑 → [⊊] Or 𝑍)    ⇒   ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃)
Theorem	ssdifidl 33404*	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 33405*	If the set 𝑆 of ssdifidl 33404 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.40  Maximal Ideals
Syntax	cmxidl 33406	Extend class notation with the class of maximal ideals.
class MaxIdeal
Definition	df-mxidl 33407*	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 33408*	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 33409*	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 33410	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 33411	A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ≠ 𝐵)
Theorem	mxidlmax 33412	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 33413	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 33414	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 33415	An ideal 𝐼 strictly containing a maximal ideal 𝑀 is the whole ring 𝐵. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑀 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐼 ∖ 𝑀))    ⇒   ⊢ (𝜑 → 𝐼 = 𝐵)
Theorem	crngmxidl 33416	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 33417	Every maximal ideal is prime. Statement in [Lang] p. 92. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ × = (LSSum‘(mulGrp‘𝑅))    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (PrmIdeal‘𝑅))
Theorem	mxidlirredi 33418	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 33419	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 33420*	The set 𝑃 used in the proof of ssmxidl 33421 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝)}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐼 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝑃)    &   ⊢ (𝜑 → 𝑍 ≠ ∅)    &   ⊢ (𝜑 → [⊊] Or 𝑍)    ⇒   ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃)
Theorem	ssmxidl 33421*	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 33422	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 33423	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 33424	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 33425	If a ring's only maximal ideal is the zero ideal, it is a division ring. See also drngmxidl 33424. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑀 = (MaxIdeal‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 = {{ 0 }})    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	krull 33426*	Krull's theorem: Any nonzero ring has at least one maximal ideal. (Contributed by Thierry Arnoux, 10-Apr-2024.)
⊢ (𝑅 ∈ NzRing → ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅))
Theorem	mxidlnzrb 33427*	A ring is nonzero if and only if it has maximal ideals. (Contributed by Thierry Arnoux, 10-Apr-2024.)
⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅)))
Theorem	krullndrng 33428*	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 33429	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 33430	Group coset equivalence relation for the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐵) → (𝑅 ~QG 𝐼) = (𝑂 ~QG 𝐼))
Theorem	opprnsg 33431	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 33432	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 33433	Two sided ideal of the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (2Ideal‘𝑅) = (2Ideal‘𝑂))
Theorem	opprmxidlabs 33434	The maximal ideal of the opposite ring's opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅))    ⇒   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘(oppr‘𝑂)))
Theorem	opprqusbas 33435	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 33436	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 33437	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 33438	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 33439	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 33440	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 33441*	Lemma for qsdrngi 33442. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑂))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑅))    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ (Base‘𝑄)(𝑣(.r‘𝑄)[𝑋](𝑅 ~QG 𝑀)) = (1r‘𝑄))
Theorem	qsdrngi 33442	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 33443	Lemma for qsdrng 33444. (Contributed by Thierry Arnoux, 13-Mar-2025.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 ∈ (2Ideal‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ DivRing)    &   ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅))    &   ⊢ (𝜑 → 𝑀 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐽 ∖ 𝑀))    ⇒   ⊢ (𝜑 → 𝐽 = 𝐵)
Theorem	qsdrng 33444	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 33445	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 33446	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.41  The semiring of ideals of a ring
Syntax	cidlsrg 33447	Extend class notation with the semiring of ideals of a ring.
class IDLsrg
Definition	df-idlsrg 33448*	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 33449	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 33450*	Lemma for idlsrgbas 33451 through idlsrgtset 33455. (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 33451	Base of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝐼 = (Base‘𝑆))
Theorem	idlsrgplusg 33452	Additive operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ ⊕ = (LSSum‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → ⊕ = (+g‘𝑆))
Theorem	idlsrg0g 33453	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 33454*	Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐵 = (LIdeal‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ ⊗ = (LSSum‘𝐺)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) = (.r‘𝑆))
Theorem	idlsrgtset 33455*	Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝐽 = (TopSet‘𝑆))
Theorem	idlsrgmulrval 33456	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 33457	Ideals of a ring 𝑅 are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    &   ⊢ 𝐵 = (LIdeal‘𝑅)    &   ⊢ ⊗ = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼 ⊗ 𝐽) ∈ 𝐵)
Theorem	idlsrgmulrss1 33458	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 33459	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 33460	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 33461	The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑆 ∈ Mnd)
Theorem	idlsrgcmnd 33462	The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝑆 = (IDLsrg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑆 ∈ CMnd)
21.3.10.42  Prime Elements
Theorem	rprmval 33463*	The prime elements of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (RPrime‘𝑅) = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))})
Theorem	isrprm 33464*	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 33465	A ring prime is an element of the base set. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	rprmdvds 33466	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 33467	A ring prime is nonzero. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝑄 ≠ 0 )
Theorem	rprmnunit 33468	A ring prime is not a unit. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → ¬ 𝑄 ∈ 𝑈)
Theorem	rsprprmprmidl 33469	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 33470	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 33471	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 33472	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 33473	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 33474*	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 33475	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 33476	A ring prime element does not divide any ring unit. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ¬ 𝑄 ∥ 𝑇)
Theorem	rprmirredlem 33477	Lemma for rprmirred 33478. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑄 ≠ 0 )    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑈))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 = (𝑋 · 𝑌))    &   ⊢ (𝜑 → 𝑄 ∥ 𝑋)    ⇒   ⊢ (𝜑 → 𝑌 ∈ 𝑈)
Theorem	rprmirred 33478	In an integral domain, ring primes are irreducible. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑄 ∈ 𝐼)
Theorem	rprmirredb 33479	In a principal ideal domain, the converse of rprmirred 33478 holds, i.e. irreducible elements are prime. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ PID)    ⇒   ⊢ (𝜑 → 𝐼 = 𝑃)
Theorem	rprmdvdspow 33480	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 33481*	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 33482*	Lemma for 1arithidom 33484. (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 33483*	Lemma for 1arithidom 33484: 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 33484*	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 16857. 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 · (𝐹 ∘ 𝑤))))
21.3.10.43  Unique factorization domains
Syntax	cufd 33485	Class of unique factorization domains.
class UFD
Definition	df-ufd 33486*	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 33487*	The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.)
⊢ 𝐼 = (PrmIdeal‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑖 ∈ (𝐼 ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅))
Theorem	ufdprmidl 33488*	In a unique factorization domain 𝑅, a nonzero prime ideal 𝐽 contains a prime element 𝑝. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐼 = (PrmIdeal‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐽 ≠ { 0 })    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ 𝑃 𝑝 ∈ 𝐽)
Theorem	ufdidom 33489	A nonzero unique factorization domain is an integral domain. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (𝜑 → 𝑅 ∈ UFD)    ⇒   ⊢ (𝜑 → 𝑅 ∈ IDomn)
Theorem	pidufd 33490	Every principal ideal domain is a unique factorization domain. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (𝜑 → 𝑅 ∈ PID)    ⇒   ⊢ (𝜑 → 𝑅 ∈ UFD)
Theorem	1arithufdlem1 33491*	Lemma for 1arithufd 33495. The set 𝑆 of elements which can be written as a product of primes is not empty. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)    &   ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}    ⇒   ⊢ (𝜑 → 𝑆 ≠ ∅)
Theorem	1arithufdlem2 33492*	Lemma for 1arithufd 33495. The set 𝑆 of elements which can be written as a product of primes is multiplicatively closed. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)    &   ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑆)
Theorem	1arithufdlem3 33493*	Lemma for 1arithufd 33495. If a product (𝑌 · 𝑋) can be written as a product of primes, with 𝑋 non-unit, nonzero, so can 𝑋. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)    &   ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑌 · 𝑋) ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑆)
Theorem	1arithufdlem4 33494*	Lemma for 1arithufd 33495. Nonzero ring, non-field case. Those trivial cases are handled in the final proof. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)    &   ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑆)
Theorem	1arithufd 33495*	Existence of a factorization into irreducible elements in a unique factorization domain. Any non-zero, non-unit element 𝑋 of a UFD 𝑅 can be written as a product of primes 𝑓. As shown in 1arithidom 33484, that factorization is unique, up to the order of the factors and multiplication by units. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ UFD)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ Word 𝑃𝑋 = (𝑀 Σg 𝑓))
Theorem	dfufd2lem 33496	Lemma for dfufd2 33497. (Contributed by Thierry Arnoux, 6-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐼 ∈ (PrmIdeal‘𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝑃)    &   ⊢ (𝜑 → (𝑀 Σg 𝐹) ∈ 𝐼)    &   ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼 ∩ 𝑃) ≠ ∅)
Theorem	dfufd2 33497*	Alternative definition of unique factorization domain (UFD). This is often the textbook definition. Chapter VII, Paragraph 3, Section 3, Proposition 2 of [BourbakiCAlg2], p. 228. (Contributed by Thierry Arnoux, 6-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑃 = (RPrime‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)))
21.3.10.44  The ring of integers
Theorem	zringidom 33498	The ring of integers is an integral domain. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ ℤring ∈ IDomn
Theorem	zringpid 33499	The ring of integers is a principal ideal domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ ℤring ∈ PID
Theorem	dfprm3 33500	The (positive) prime elements of the integer ring are the prime numbers. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ ℙ = (ℕ ∩ (RPrime‘ℤring))