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	isunitc 33501*	Characterize units in a commutative ring. (Contributed by Thierry Arnoux, 6-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ ∃𝑦 ∈ 𝐵 (𝑋 · 𝑦) = 1 ))
21.3.10.19  Subrings generated by a set
Theorem	elrgspnlem1 33502*	Lemma for elrgspn 33506. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))    ⇒   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅))
Theorem	elrgspnlem2 33503*	Lemma for elrgspn 33506. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))    ⇒   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))
Theorem	elrgspnlem3 33504*	Lemma for elrgspn 33506. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)
Theorem	elrgspnlem4 33505*	Lemma for elrgspn 33506. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.g‘𝑅)    &   ⊢ 𝑁 = (RingSpan‘𝑅)    &   ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))    ⇒   ⊢ (𝜑 → (𝑁‘𝐴) = 𝑆)
Theorem	elrgspn 33506*	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 33507*	Lemma for elrgspnsubrun 33509, 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 33508*	Lemma for elrgspnsubrun 33509, 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 33509*	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 33510	A ring with an irreducible element cannot be the zero ring. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ 𝐼 = (Irred‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → 𝑅 ∈ NzRing)
Theorem	0ringsubrg 33511	A subring of a zero ring is a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → (♯‘𝐵) = 1)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (♯‘𝑆) = 1)
Theorem	0ringcring 33512	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 33513	Syntax for ring localization equivalence class operation.
class ~RL
Syntax	crloc 33514	Syntax for ring localization operation.
class RLocal
Definition	df-erl 33515*	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 33516*	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 33517	Ring localization is a proper operator, so it can be used with ovprc1 7450. (Contributed by Thierry Arnoux, 10-May-2025.)
⊢ Rel dom RLocal
Theorem	erlval 33518*	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 33519*	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 33520	Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∼ 𝑉)    ⇒   ⊢ (𝜑 → 𝑈 ∈ (𝐵 × 𝑆))
Theorem	erlcl2 33521	Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∼ 𝑉)    ⇒   ⊢ (𝜑 → 𝑉 ∈ (𝐵 × 𝑆))
Theorem	erldi 33522*	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 33523	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 33524	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 33525	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	erld2 33526*	Main property of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑆)    &   ⊢ (𝜑 → [⟨𝑋, 𝑌⟩] ∼ = [⟨𝑍, 𝑊⟩] ∼ )    ⇒   ⊢ (𝜑 → ∃𝑡 ∈ 𝑆 (𝑡 · (𝑋 · 𝑊)) = (𝑡 · (𝑍 · 𝑌)))
Theorem	elrlocbasi 33527*	Membership in the basis of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝑋 ∈ ((𝐵 × 𝑆) / ∼ ))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝑆 𝑋 = [⟨𝑎, 𝑏⟩] ∼ )
Theorem	rlocbas 33528	The base set of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ 𝑊 = (𝐵 × 𝑆)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑊 / ∼ ) = (Base‘𝐿))
Theorem	rlocaddval 33529	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 33530	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 33531	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 33532	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 33533	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 33534*	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 𝐿)))
Theorem	rlocinvunit 33535	In the localization of a ring 𝑅 at 𝑆, inverses of elements of 𝑆 are units. (Contributed by Thierry Arnoux, 6-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ 𝑊 = (Unit‘𝐿)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    ⇒   ⊢ (𝜑 → [⟨ 1 , 𝑄⟩] ∼ ∈ 𝑊)
Theorem	rlocisunit 33536*	Characterize the units of the localization 𝐿 of a ring 𝑅 at 𝑆 as the elements with a "numerator" 𝑃 in the saturation 𝑇 of 𝑆. (Contributed by Thierry Arnoux, 6-Jun-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐿 = (𝑅 RLocal 𝑆)    &   ⊢ 𝑊 = (Unit‘𝐿)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))    &   ⊢ ∼ = (𝑅 ~RL 𝑆)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    &   ⊢ 𝑇 = {𝑟 ∈ 𝐵 ∣ ∃𝑠 ∈ 𝐵 (𝑟 · 𝑠) ∈ 𝑆}    ⇒   ⊢ (𝜑 → ([⟨𝑃, 𝑄⟩] ∼ ∈ 𝑊 ↔ 𝑃 ∈ 𝑇))
21.3.10.22  Integral Domains
Theorem	domnmuln0rd 33537	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 33538	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	domnprodeq0 33539	A product over a domain is zero exactly when one of the factors is zero. Generalization of domneq0 20792 for any number of factors. See also domnprodn0 33538. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹) = 0 ↔ 0 ∈ ran 𝐹))
Theorem	domnpropd 33540*	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 33541*	If two structures have the same components (properties), one is a integral domain iff the other one is. See also domnpropd 33540. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ IDomn ↔ 𝐿 ∈ IDomn))
Theorem	idomrcan 33542	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	1rrg 33543	The multiplicative identity is a left-regular element. (Contributed by Thierry Arnoux, 6-May-2025.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 1 ∈ 𝐸)
Theorem	rrgsubm 33544	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 33545	A subring of a domain is a domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Domn)
Theorem	subridom 33546	A subring of an integral domain is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn)
Theorem	subrfld 33547	A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ (𝜑 → 𝑅 ∈ Field)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn)
Theorem	ricnzr1 33548	A ring isomorphism maps a nonzero ring to a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing) → 𝑆 ∈ NzRing)
Theorem	ricdomn1 33549	A ring isomorphism maps a domain to a domain. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn) → 𝑆 ∈ Domn)
Theorem	ricdomn 33550	A ring is a domain if and only if an isomorphic ring is a domain. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ Domn ↔ 𝑆 ∈ Domn))
21.3.10.23  Euclidean Domains
Syntax	ceuf 33551	Declare the syntax for the Euclidean function index extractor.
class EuclF
Definition	df-euf 33552	Define the Euclidean function. (Contributed by Thierry Arnoux, 22-Mar-2025.) Use its index-independent form eufid 33554 instead. (New usage is discouraged.)
⊢ EuclF = Slot ;21
Theorem	eufndx 33553	Index value of the Euclidean function slot. Use ndxarg 17255. (Contributed by Thierry Arnoux, 22-Mar-2025.) (New usage is discouraged.)
⊢ (EuclF‘ndx) = ;21
Theorem	eufid 33554	Utility theorem: index-independent form of df-euf 33552. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ EuclF = Slot (EuclF‘ndx)
Syntax	cedom 33555	Declare the syntax for the Euclidean Domain.
class EDomn
Definition	df-edom 33556*	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 33557	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 33558*	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 33559	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 33560	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 33561	A subring of a sub-division-ring is a sub-division-ring. See also subsubrg 20682. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝐵 ∈ (SubDRing‘𝑆) ↔ (𝐵 ∈ (SubDRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)))
Theorem	sdrgdvcl 33562	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 33563	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 33564	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 33565	Syntax for the field of fractions of a given integral domain.
class Frac
Definition	df-frac 33566	Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025.)
⊢ Frac = (𝑟 ∈ V ↦ (𝑟 RLocal (RLReg‘𝑟)))
Theorem	fracval 33567	Value of the field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.)
⊢ ( Frac ‘𝑅) = (𝑅 RLocal (RLReg‘𝑅))
Theorem	fracbas 33568	The base of the field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐹 = ( Frac ‘𝑅)    &   ⊢ ∼ = (𝑅 ~RL 𝐸)    ⇒   ⊢ ((𝐵 × 𝐸) / ∼ ) = (Base‘𝐹)
Theorem	fracerl 33569	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 33570*	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 33571	The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → ( Frac ‘𝑅) ∈ Field)
Theorem	idomsubr 33572*	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 33573	Syntax for a function generating sub-fields.
class fldGen
Definition	df-fldgen 33574*	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 33577). If the base structure is a field, this is a subfield (see fldgenfld 33583 and fldsdrgfld 20878). 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 33575*	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 33576	The field generated by a set of elements contains those elements. See lspssid 21083. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ (𝐹 fldGen 𝑆))
Theorem	fldgensdrg 33577	A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) ∈ (SubDRing‘𝐹))
Theorem	fldgenssv 33578	A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) ⊆ 𝐵)
Theorem	fldgenss 33579	Generated subfields preserve subset ordering. ( see lspss 21082 and spanss 31640) (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ (𝐹 fldGen 𝑆))
Theorem	fldgenidfld 33580	The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹))    ⇒   ⊢ (𝜑 → (𝐹 fldGen 𝑆) = 𝑆)
Theorem	fldgenssp 33581	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 33582	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 33583	A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ↾s (𝐹 fldGen 𝑆)) ∈ Field)
Theorem	primefldgen1 33584	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 33585	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  Ring homomorphisms - misc additions
Theorem	rhmdvd 33586	A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ 𝑈 = (Unit‘𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ / = (/r‘𝑆)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ ((𝐹‘𝐵) ∈ 𝑈 ∧ (𝐹‘𝐶) ∈ 𝑈)) → ((𝐹‘𝐴) / (𝐹‘𝐵)) = ((𝐹‘(𝐴 · 𝐶)) / (𝐹‘(𝐵 · 𝐶))))
Theorem	kerunit 33587	If a unit element lies in the kernel of a ring homomorphism, then 0 = 1, i.e. the target ring is the zero ring. (Contributed by Thierry Arnoux, 24-Oct-2017.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 1 = (1r‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝑈 ∩ (◡𝐹 “ { 0 })) ≠ ∅) → 1 = 0 )
21.3.10.30  Scalar restriction operation
Syntax	cresv 33588	Extend class notation with the scalar restriction operation.
class ↾v
Definition	df-resv 33589*	Define an operator to restrict the scalar field component of an extended structure. (Contributed by Thierry Arnoux, 5-Sep-2018.)
⊢ ↾v = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩)))
Theorem	reldmresv 33590	The scalar restriction is a proper operator, so it can be used with ovprc1 7450. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ Rel dom ↾v
Theorem	resvval 33591	Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩)))
Theorem	resvid2 33592	General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊)
Theorem	resvval2 33593	Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩))
Theorem	resvsca 33594	Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅))
Theorem	resvlem 33595	Other elements of a scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝑅 = (𝑊 ↾v 𝐴)    &   ⊢ 𝐶 = (𝐸‘𝑊)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (Scalar‘ndx)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐶 = (𝐸‘𝑅))
Theorem	resvbas 33596	Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻))
Theorem	resvplusg 33597	+g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻))
Theorem	resvvsca 33598	·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻))
Theorem	resvmulr 33599	.r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ · = (.r‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻))
Theorem	resv0g 33600	0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
⊢ 𝐻 = (𝐺 ↾v 𝐴)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻))