P. 333 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33201-33300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elrgspnlem2 33201*	Lemma for elrgspn 33204. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))    ⇒   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))
Theorem	elrgspnlem3 33202*	Lemma for elrgspn 33204. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)
Theorem	elrgspnlem4 33203*	Lemma for elrgspn 33204. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))    ⇒   ⊢ (𝜑 → (𝑁‘𝐴) = 𝑆)
Theorem	elrgspn 33204*	Membership in the subring generated by the subset 𝐴. An element 𝑋 lies in that subring if and only if 𝑋 is a linear combination with integer coefficients of products of elements of 𝐴. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝐴) ↔ ∃𝑔 ∈ 𝐹 𝑋 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
Theorem	elrgspnsubrunlem1 33205*	Lemma for elrgspnsubrun 33207, first direction. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐸 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑃:𝐹⟶𝐸)    &   ⊢ (𝜑 → 𝑃 finSupp 0 )    &   ⊢ (𝜑 → 𝑋 = (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒))))    &   ⊢ 𝑇 = ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹)))
Theorem	elrgspnsubrunlem2 33206*	Lemma for elrgspnsubrun 33207, second direction. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐸 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺:Word (𝐸 ∪ 𝐹)⟶ℤ)    &   ⊢ (𝜑 → 𝐺 finSupp 0)    &   ⊢ (𝜑 → 𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝐺‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ (𝐸 ↑m 𝐹)(𝑝 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑓 ∈ 𝐹 ↦ ((𝑝‘𝑓) · 𝑓)))))
Theorem	elrgspnsubrun 33207*	Membership in the ring span of the union of two subrings of a commutative ring. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐸 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹)) ↔ ∃𝑝 ∈ (𝐸 ↑m 𝐹)(𝑝 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑓 ∈ 𝐹 ↦ ((𝑝‘𝑓) · 𝑓))))))
21.3.10.20  The zero ring
Theorem	irrednzr 33208	A ring with an irreducible element cannot be the zero ring. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → 𝑅 ∈ NzRing)
Theorem	0ringsubrg 33209	A subring of a zero ring is a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → (♯‘𝐵) = 1)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (♯‘𝑆) = 1)
Theorem	0ringcring 33210	The zero ring is commutative. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → (♯‘𝐵) = 1)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
21.3.10.21  Localization of rings
Syntax	cerl 33211	Syntax for ring localization equivalence class operation.
class ~RL
Syntax	crloc 33212	Syntax for ring localization operation.
class RLocal
Definition	df-erl 33213*	Define the operation giving the equivalence relation used in the localization of a ring 𝑟 by a set 𝑠. Two pairs 𝑎 = ⟨𝑥, 𝑦⟩ and 𝑏 = ⟨𝑧, 𝑤⟩ are equivalent if there exists 𝑡 ∈ 𝑠 such that 𝑡 · (𝑥 · 𝑤 − 𝑧 · 𝑦) = 0. This corresponds to the usual comparison of fractions 𝑥 / 𝑦 and 𝑧 / 𝑤. (Contributed by Thierry Arnoux, 28-Apr-2025.)
⊢ ~RL = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))})
Definition	df-rloc 33214*	Define the operation giving the localization of a ring 𝑟 by a given set 𝑠. The localized ring 𝑟 RLocal 𝑠 is the set of equivalence classes of pairs of elements in 𝑟 over the relation 𝑟 ~RL 𝑠 with addition and multiplication defined naturally. (Contributed by Thierry Arnoux, 27-Apr-2025.)
⊢ RLocal = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) /s (𝑟 ~RL 𝑠)))
Theorem	reldmrloc 33215	Ring localization is a proper operator, so it can be used with ovprc1 7429. (Contributed by Thierry Arnoux, 10-May-2025.)
⊢ Rel dom RLocal
Theorem	erlval 33216*	Value of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ 𝑊 = (𝐵 × 𝑆)    &   ⊢ ∼ = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st ‘𝑎) · (2nd ‘𝑏)) − ((1st ‘𝑏) · (2nd ‘𝑎)))) = 0 )}    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑅 ~RL 𝑆) = ∼ )
Theorem	rlocval 33217*	Expand the value of the ring localization operation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    &   ⊢ 𝐹 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝐶 = ( ·𝑠 ‘𝑅)    &   ⊢ 𝑊 = (𝐵 × 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ 𝐽 = (TopSet‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑅)    &   ⊢ ⊕ = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)    &   ⊢ ⊗ = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)    &   ⊢ × = (𝑘 ∈ 𝐾, 𝑎 ∈ 𝑊 ↦ ⟨(𝑘𝐶(1st ‘𝑎)), (2nd ‘𝑎)⟩)    &   ⊢ ≲ = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd ‘𝑏)) ≤ ((1st ‘𝑏) · (2nd ‘𝑎)))}    &   ⊢ 𝐸 = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ (((1st ‘𝑎) · (2nd ‘𝑏))𝐷((1st ‘𝑏) · (2nd ‘𝑎))))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑅 RLocal 𝑆) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ∼ ))
Theorem	erlcl1 33218	Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∼ 𝑉)    ⇒   ⊢ (𝜑 → 𝑈 ∈ (𝐵 × 𝑆))
Theorem	erlcl2 33219	Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∼ 𝑉)    ⇒   ⊢ (𝜑 → 𝑉 ∈ (𝐵 × 𝑆))
Theorem	erldi 33220*	Main property of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∼ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑡 ∈ 𝑆 (𝑡 · (((1st ‘𝑈) · (2nd ‘𝑉)) − ((1st ‘𝑉) · (2nd ‘𝑈)))) = 0 )
Theorem	erlbrd 33221	Deduce the ring localization equivalence relation. If for some 𝑇 ∈ 𝑆 we have 𝑇 · (𝐸 · 𝐻 − 𝐹 · 𝐺) = 0, then pairs ⟨𝐸, 𝐺⟩ and ⟨𝐹, 𝐻⟩ are equivalent under the localization relation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ (𝜑 → 𝑈 = ⟨𝐸, 𝐺⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨𝐹, 𝐻⟩)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → (𝑇 · ((𝐸 · 𝐻) − (𝐹 · 𝐺))) = 0 )    ⇒   ⊢ (𝜑 → 𝑈 ∼ 𝑉)
Theorem	erlbr2d 33222	Deduce the ring localization equivalence relation. Pairs ⟨𝐸, 𝐺⟩ and ⟨𝑇 · 𝐸, 𝑇 · 𝐺⟩ for 𝑇 ∈ 𝑆 are equivalent under the localization relation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑈 = ⟨𝐸, 𝐺⟩)    &   ⊢ (𝜑 → 𝑉 = ⟨𝐹, 𝐻⟩)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 = (𝑇 · 𝐸))    &   ⊢ (𝜑 → 𝐻 = (𝑇 · 𝐺))    ⇒   ⊢ (𝜑 → 𝑈 ∼ 𝑉)
Theorem	erler 33223	The relation used to build the ring localization is an equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ 𝑊 = (𝐵 × 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    ⇒   ⊢ (𝜑 → ∼ Er 𝑊)
Theorem	elrlocbasi 33224*	Membership in the basis of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝑋 ∈ ((𝐵 × 𝑆) / ∼ ))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝑆 𝑋 = [⟨𝑎, 𝑏⟩] ∼ )
Theorem	rlocbas 33225	The base set of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ 𝑊 = (𝐵 × 𝑆)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑊 / ∼ ) = (Base‘𝐿))
Theorem	rlocaddval 33226	Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑆)    &   ⊢ ⊕ = (+g‘𝐿)    ⇒   ⊢ (𝜑 → ([⟨𝐸, 𝐺⟩] ∼ ⊕ [⟨𝐹, 𝐻⟩] ∼ ) = [⟨((𝐸 · 𝐻) + (𝐹 · 𝐺)), (𝐺 · 𝐻)⟩] ∼ )
Theorem	rlocmulval 33227	Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑆)    &   ⊢ ⊗ = (.r‘𝐿)    ⇒   ⊢ (𝜑 → ([⟨𝐸, 𝐺⟩] ∼ ⊗ [⟨𝐹, 𝐻⟩] ∼ ) = [⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩] ∼ )
Theorem	rloccring 33228	The ring localization 𝐿 of a commutative ring 𝑅 by a multiplicatively closed set 𝑆 is itself a commutative ring. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    ⇒   ⊢ (𝜑 → 𝐿 ∈ CRing)
Theorem	rloc0g 33229	The zero of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ 𝑂 = [⟨ 0 , 1 ⟩] ∼    ⇒   ⊢ (𝜑 → 𝑂 = (0g‘𝐿))
Theorem	rloc1r 33230	The multiplicative identity of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ 𝐼 = [⟨ 1 , 1 ⟩] ∼    ⇒   ⊢ (𝜑 → 𝐼 = (1r‘𝐿))
Theorem	rlocf1 33231*	The embedding 𝐹 of a ring 𝑅 into its localization 𝐿. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [⟨𝑥, 1 ⟩] ∼ )    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ (𝜑 → 𝑆 ⊆ (RLReg‘𝑅))    ⇒   ⊢ (𝜑 → (𝐹:𝐵–1-1→((𝐵 × 𝑆) / ∼ ) ∧ 𝐹 ∈ (𝑅 RingHom 𝐿)))
21.3.10.22  Integral Domains
Theorem	domnmuln0rd 33232	In a domain, factors of a nonzero product are nonzero. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 · 𝑌) ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ))
Theorem	domnprodn0 33233	In a domain, a finite product of nonzero terms is nonzero. (Contributed by Thierry Arnoux, 6-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝐹 ∈ Word (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0 )
Theorem	domnpropd 33234*	If two structures have the same components (properties), one is a domain iff the other one is. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Domn ↔ 𝐿 ∈ Domn))
Theorem	idompropd 33235*	If two structures have the same components (properties), one is a integral domain iff the other one is. See also domnpropd 33234. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ IDomn ↔ 𝐿 ∈ IDomn))
Theorem	idomrcan 33236	Right-cancellation law for integral domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) (Proof shortened by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	domnlcanOLD 33237	Obsolete version of domnlcan 20637 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 22-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 · 𝑍))    ⇒   ⊢ (𝜑 → 𝑌 = 𝑍)
Theorem	domnlcanbOLD 33238	Obsolete version of domnlcanb 20636 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 8-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = (𝑋 · 𝑍) ↔ 𝑌 = 𝑍))
Theorem	idomrcanOLD 33239	Obsolete version of idomrcan 33236 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 22-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → (𝑌 · 𝑋) = (𝑍 · 𝑋))    ⇒   ⊢ (𝜑 → 𝑌 = 𝑍)
Theorem	1rrg 33240	The multiplicative identity is a left-regular element. (Contributed by Thierry Arnoux, 6-May-2025.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 1 ∈ 𝐸)
Theorem	rrgsubm 33241	The left regular elements of a ring form a submonoid of the multiplicative group. (Contributed by Thierry Arnoux, 10-May-2025.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝐸 ∈ (SubMnd‘𝑀))
Theorem	subrdom 33242	A subring of a domain is a domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Domn)
Theorem	subridom 33243	A subring of an integral domain is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn)
Theorem	subrfld 33244	A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ (𝜑 → 𝑅 ∈ Field)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn)
21.3.10.23  Euclidean Domains
Syntax	ceuf 33245	Declare the syntax for the Euclidean function index extractor.
class EuclF
Definition	df-euf 33246	Define the Euclidean function. (Contributed by Thierry Arnoux, 22-Mar-2025.) Use its index-independent form eufid 33248 instead. (New usage is discouraged.)
⊢ EuclF = Slot ;21
Theorem	eufndx 33247	Index value of the Euclidean function slot. Use ndxarg 17173. (Contributed by Thierry Arnoux, 22-Mar-2025.) (New usage is discouraged.)
⊢ (EuclF‘ndx) = ;21
Theorem	eufid 33248	Utility theorem: index-independent form of df-euf 33246. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ EuclF = Slot (EuclF‘ndx)
Syntax	cedom 33249	Declare the syntax for the Euclidean Domain.
class EDomn
Definition	df-edom 33250*	Define Euclidean Domains. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ EDomn = {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣](Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))}
21.3.10.24  Division Rings
Theorem	ringinveu 33251	If a ring unit element 𝑋 admits both a left inverse 𝑌 and a right inverse 𝑍, they are equal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑌 · 𝑋) = 1 )    &   ⊢ (𝜑 → (𝑋 · 𝑍) = 1 )    ⇒   ⊢ (𝜑 → 𝑍 = 𝑌)
Theorem	isdrng4 33252*	A division ring is a ring in which 1 ≠ 0 and every nonzero element has a left and right inverse. (Contributed by Thierry Arnoux, 2-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝑅 ∈ DivRing ↔ ( 1 ≠ 0 ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ))))
Theorem	rndrhmcl 33253	The image of a division ring by a ring homomorphism is a division ring. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝑅 = (𝑁 ↾s ran 𝐹)    &   ⊢ 0 = (0g‘𝑁)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁))    &   ⊢ (𝜑 → ran 𝐹 ≠ { 0 })    &   ⊢ (𝜑 → 𝑀 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
21.3.10.25  The field of rational numbers
Theorem	qfld 33254	The field of rational numbers is a field. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 𝑄 ∈ Field
21.3.10.26  Subfields
Theorem	subsdrg 33255	A subring of a sub-division-ring is a sub-division-ring. See also subsubrg 20514. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝐵 ∈ (SubDRing‘𝑆) ↔ (𝐵 ∈ (SubDRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)))
Theorem	sdrgdvcl 33256	A sub-division-ring is closed under the ring division operation. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ / = (/r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 / 𝑌) ∈ 𝐴)
Theorem	sdrginvcl 33257	A sub-division-ring is closed under the ring inverse operation. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubDRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ∈ 𝐴)
Theorem	primefldchr 33258	The characteristic of a prime field is the same as the characteristic of the main field. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝑃 = (𝑅 ↾s ∩ (SubDRing‘𝑅))    ⇒   ⊢ (𝑅 ∈ DivRing → (chr‘𝑃) = (chr‘𝑅))
21.3.10.27  Field of fractions
Syntax	cfrac 33259	Syntax for the field of fractions of a given integral domain.
class Frac
Definition	df-frac 33260	Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025.)
⊢ Frac = (𝑟 ∈ V ↦ (𝑟 RLocal (RLReg‘𝑟)))
Theorem	fracval 33261	Value of the field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.)
⊢ ( Frac ‘𝑅) = (𝑅 RLocal (RLReg‘𝑅))
Theorem	fracbas 33262	The base of the field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐹 = ( Frac ‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝐸)    ⇒   ⊢ ((𝐵 × 𝐸) / ∼ ) = (Base‘𝐹)
Theorem	fracerl 33263	Rewrite the ring localization equivalence relation in the case of a field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL (RLReg‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (RLReg‘𝑅))    &   ⊢ (𝜑 → 𝐻 ∈ (RLReg‘𝑅))    ⇒   ⊢ (𝜑 → (⟨𝐸, 𝐹⟩ ∼ ⟨𝐺, 𝐻⟩ ↔ (𝐸 · 𝐻) = (𝐺 · 𝐹)))
Theorem	fracf1 33264*	The embedding of a commutative ring 𝑅 into its field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ∼ = (𝑅 ~RL 𝐸)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [⟨𝑥, 1 ⟩] ∼ )    ⇒   ⊢ (𝜑 → (𝐹:𝐵–1-1→((𝐵 × 𝐸) / ∼ ) ∧ 𝐹 ∈ (𝑅 RingHom ( Frac ‘𝑅))))
Theorem	fracfld 33265	The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → ( Frac ‘𝑅) ∈ Field)
Theorem	idomsubr 33266*	Every integral domain is isomorphic with a subring of some field. (Proposed by Gerard Lang, 10-May-2025.) (Contributed by Thierry Arnoux, 10-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ Field ∃𝑠 ∈ (SubRing‘𝑓)𝑅 ≃𝑟 (𝑓 ↾s 𝑠))
21.3.10.28  Field extensions generated by a set
Syntax	cfldgen 33267	Syntax for a function generating sub-fields.
class fldGen
Definition	df-fldgen 33268*	Define a function generating the smallest sub-division-ring of a given ring containing a given set. If the base structure is a division ring, then this is also a division ring (see fldgensdrg 33271). If the base structure is a field, this is a subfield (see fldgenfld 33277 and fldsdrgfld 20714). In general this will be used in the context of fields, hence the name fldGen. (Contributed by Saveliy Skresanov and Thierry Arnoux, 9-Jan-2025.)
⊢ fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎})
Theorem	fldgenval 33269*	Value of the field generating function: (𝐹 fldGen 𝑆) is the smallest sub-division-ring of 𝐹 containing 𝑆. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) = ∩ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎})
Theorem	fldgenssid 33270	The field generated by a set of elements contains those elements. See lspssid 20898. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ (𝐹 fldGen 𝑆))
Theorem	fldgensdrg 33271	A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) ∈ (SubDRing‘𝐹))
Theorem	fldgenssv 33272	A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) ⊆ 𝐵)
Theorem	fldgenss 33273	Generated subfields preserve subset ordering. ( see lspss 20897 and spanss 31284) (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ (𝐹 fldGen 𝑆))
Theorem	fldgenidfld 33274	The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹))    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) = 𝑆)
Theorem	fldgenssp 33275	The field generated by a set of elements in a division ring is contained in any sub-division-ring which contains those elements. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹))    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ 𝑆)
Theorem	fldgenid 33276	The subfield of a field 𝐹 generated by the whole base set of 𝐹 is 𝐹 itself. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝐵) = 𝐵)
Theorem	fldgenfld 33277	A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ↾s (𝐹 fldGen 𝑆)) ∈ Field)
Theorem	primefldgen1 33278	The prime field of a division ring is the subfield generated by the multiplicative identity element. In general, we should write "prime division ring", but since most later usages are in the case where the ambient ring is commutative, we keep the term "prime field". (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → ∩ (SubDRing‘𝑅) = (𝑅 fldGen { 1 }))
Theorem	1fldgenq 33279	The field of rational numbers ℚ is generated by 1 in ℂfld, that is, ℚ is the prime field of ℂfld. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ (ℂfld fldGen {1}) = ℚ
21.3.10.29  Totally ordered rings and fields
Syntax	corng 33280	Extend class notation with the class of all ordered rings.
class oRing
Syntax	cofld 33281	Extend class notation with the class of all ordered fields.
class oField
Definition	df-orng 33282*	Define class of all ordered rings. An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ oRing = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
Definition	df-ofld 33283	Define class of all ordered fields. An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.)
⊢ oField = (Field ∩ oRing)
Theorem	isorng 33284*	An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    ⇒   ⊢ (𝑅 ∈ oRing ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏))))
Theorem	orngring 33285	An ordered ring is a ring. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Ring)
Theorem	orngogrp 33286	An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oGrp)
Theorem	isofld 33287	An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (𝐹 ∈ oField ↔ (𝐹 ∈ Field ∧ 𝐹 ∈ oRing))
Theorem	orngmul 33288	In an ordered ring, the ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ oRing ∧ (𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ 𝐵 ∧ 0 ≤ 𝑌)) → 0 ≤ (𝑋 · 𝑌))
Theorem	orngsqr 33289	In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 0 ≤ (𝑋 · 𝑋))
Theorem	ornglmulle 33290	In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ oRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝑅)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 0 ≤ 𝑍)    ⇒   ⊢ (𝜑 → (𝑍 · 𝑋) ≤ (𝑍 · 𝑌))
Theorem	orngrmulle 33291	In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ oRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝑅)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 0 ≤ 𝑍)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑍) ≤ (𝑌 · 𝑍))
Theorem	ornglmullt 33292	In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ oRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ < = (lt‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 < 𝑌)    &   ⊢ (𝜑 → 0 < 𝑍)    ⇒   ⊢ (𝜑 → (𝑍 · 𝑋) < (𝑍 · 𝑌))
Theorem	orngrmullt 33293	In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ oRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ < = (lt‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 < 𝑌)    &   ⊢ (𝜑 → 0 < 𝑍)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑍) < (𝑌 · 𝑍))
Theorem	orngmullt 33294	In an ordered ring, the strict ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 9-Sep-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ < = (lt‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ oRing)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 0 < 𝑋)    &   ⊢ (𝜑 → 0 < 𝑌)    ⇒   ⊢ (𝜑 → 0 < (𝑋 · 𝑌))
Theorem	ofldfld 33295	An ordered field is a field. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ (𝐹 ∈ oField → 𝐹 ∈ Field)
Theorem	ofldtos 33296	An ordered field is a totally ordered set. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ (𝐹 ∈ oField → 𝐹 ∈ Toset)
Theorem	orng0le1 33297	In an ordered ring, the ring unity is positive. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ 0 = (0g‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    &   ⊢ ≤ = (le‘𝐹)    ⇒   ⊢ (𝐹 ∈ oRing → 0 ≤ 1 )
Theorem	ofldlt1 33298	In an ordered field, the ring unity is strictly positive. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ 0 = (0g‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    &   ⊢ < = (lt‘𝐹)    ⇒   ⊢ (𝐹 ∈ oField → 0 < 1 )
Theorem	ofldchr 33299	The characteristic of an ordered field is zero. (Contributed by Thierry Arnoux, 21-Jan-2018.) (Proof shortened by AV, 6-Oct-2020.)
⊢ (𝐹 ∈ oField → (chr‘𝐹) = 0)
Theorem	suborng 33300	Every subring of an ordered ring is also an ordered ring. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ oRing)