P. 208 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20701-20800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isdrngrdOLD 20701*	Obsolete version of isdrngrd 20699 as of 19-Feb-2025. (Contributed by NM, 10-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 0 = (0g‘𝑅))    &   ⊢ (𝜑 → 1 = (1r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 )    &   ⊢ (𝜑 → 1 ≠ 0 )    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ≠ 0 )    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝑥 · 𝐼) = 1 )    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	drngpropd 20702*	If two structures have the same group components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 27-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing))
Theorem	fldpropd 20703*	If two structures have the same group components (properties), one is a field iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Field ↔ 𝐿 ∈ Field))
Theorem	fldidom 20704	A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof shortened by SN, 11-Nov-2024.)
⊢ (𝑅 ∈ Field → 𝑅 ∈ IDomn)
Theorem	fidomndrnglem 20705*	Lemma for fidomndrng 20706. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ { 0 }))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝐴))    ⇒   ⊢ (𝜑 → 𝐴 ∥ 1 )
Theorem	fidomndrng 20706	A finite domain is a division ring. Note that Wedderburn's little theorem (not proved) states that finite division rings are fields. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐵 ∈ Fin → (𝑅 ∈ Domn ↔ 𝑅 ∈ DivRing))
Theorem	fiidomfld 20707	A finite integral domain is a field. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐵 ∈ Fin → (𝑅 ∈ IDomn ↔ 𝑅 ∈ Field))
Theorem	rng1nnzr 20708	The (smallest) structure representing a zero ring is not a nonzero ring. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    ⇒   ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∉ NzRing)
Theorem	ring1zr 20709	The only (unital) ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption 𝑅 ∈ Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 7-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ∗ = (.r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
Theorem	rngen1zr 20710	The only (unital) ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption 𝑅 ∈ Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 25-Jan-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ∗ = (.r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 ≈ 1o ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
Theorem	ringen1zr 20711	The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption 𝑅 ∈ Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 15-Feb-2010.) (Revised by AV, 25-Jan-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) → (𝐵 ≈ 1o ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
Theorem	rng1nfld 20712	The zero ring is not a field. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    ⇒   ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∉ Field)
Theorem	issubdrg 20713*	Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → (𝑆 ∈ DivRing ↔ ∀𝑥 ∈ (𝐴 ∖ { 0 })(𝐼‘𝑥) ∈ 𝐴))
Theorem	drhmsubc 20714*	According to df-subc 17736, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17764 and subcss2 17767). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈ (Subcat‘(RingCat‘𝑈)))
Theorem	drngcat 20715*	The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCat‘𝑈) ↾cat 𝐽) ∈ Cat)
Theorem	fldcat 20716*	The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    &   ⊢ 𝐷 = (𝑈 ∩ Field)    &   ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCat‘𝑈) ↾cat 𝐹) ∈ Cat)
Theorem	fldc 20717*	The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    &   ⊢ 𝐷 = (𝑈 ∩ Field)    &   ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → (((RingCat‘𝑈) ↾cat 𝐽) ↾cat 𝐹) ∈ Cat)
Theorem	fldhmsubc 20718*	According to df-subc 17736, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17764 and subcss2 17767). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    &   ⊢ 𝐷 = (𝑈 ∩ Field)    &   ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐹 ∈ (Subcat‘((RingCat‘𝑈) ↾cat 𝐽)))
10.4.2  Sub-division rings
Syntax	csdrg 20719	Syntax for subfields (sub-division-rings).
class SubDRing
Definition	df-sdrg 20720*	Define the function associating with a ring the set of its sub-division-rings. A sub-division-ring of a ring is a subset of its base set which is a division ring when equipped with the induced structure (sum, multiplication, zero, and unity). If a ring is commutative (resp., a field), then its sub-division-rings are commutative (resp., are fields) (fldsdrgfld 20731), so we do not make a specific definition for subfields. (Contributed by Stefan O'Rear, 3-Oct-2015.) TODO: extend this definition to a function with domain V or at least Ring and not only DivRing.
⊢ SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing})
Theorem	issdrg 20721	Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.)
⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing))
Theorem	sdrgrcl 20722	Reverse closure for a sub-division-ring predicate. (Contributed by SN, 19-Feb-2025.)
⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝑅 ∈ DivRing)
Theorem	sdrgdrng 20723	A sub-division-ring is a division ring. (Contributed by SN, 19-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝑆 ∈ DivRing)
Theorem	sdrgsubrg 20724	A sub-division-ring is a subring. (Contributed by SN, 19-Feb-2025.)
⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝐴 ∈ (SubRing‘𝑅))
Theorem	sdrgid 20725	Every division ring is a division subring of itself. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → 𝐵 ∈ (SubDRing‘𝑅))
Theorem	sdrgss 20726	A division subring is a subset of the base set. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑆 ∈ (SubDRing‘𝑅) → 𝑆 ⊆ 𝐵)
Theorem	sdrgbas 20727	Base set of a sub-division-ring structure. (Contributed by SN, 19-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝐴 = (Base‘𝑆))
Theorem	issdrg2 20728*	Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑆 ∖ { 0 })(𝐼‘𝑥) ∈ 𝑆))
Theorem	sdrgunit 20729	A unit of a sub-division-ring is a nonzero element of the subring. (Contributed by SN, 19-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑆)    ⇒   ⊢ (𝐴 ∈ (SubDRing‘𝑅) → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 )))
Theorem	imadrhmcl 20730	The image of a (nontrivial) division ring homomorphism is a division ring. (Contributed by SN, 17-Feb-2025.)
⊢ 𝑅 = (𝑁 ↾s (𝐹 “ 𝑆))    &   ⊢ 0 = (0g‘𝑁)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁))    &   ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝑀))    &   ⊢ (𝜑 → ran 𝐹 ≠ { 0 })    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	fldsdrgfld 20731	A sub-division-ring of a field is itself a field, so it is a subfield. We can therefore use SubDRing to express subfields. (Contributed by Thierry Arnoux, 11-Jan-2025.)
⊢ ((𝐹 ∈ Field ∧ 𝐴 ∈ (SubDRing‘𝐹)) → (𝐹 ↾s 𝐴) ∈ Field)
Theorem	acsfn1p 20732*	Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))
Theorem	subrgacs 20733	Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (ACS‘𝐵))
Theorem	sdrgacs 20734	Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → (SubDRing‘𝑅) ∈ (ACS‘𝐵))
Theorem	cntzsdrg 20735	Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubDRing‘𝑅))
Theorem	subdrgint 20736*	The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝐿 = (𝑅 ↾s ∩ 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑆 ⊆ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑆 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑅 ↾s 𝑠) ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝐿 ∈ DivRing)
Theorem	sdrgint 20737	The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ (SubDRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubDRing‘𝑅))
Theorem	primefld 20738	The smallest sub division ring of a division ring, here named 𝑃, is a field, called the Prime Field of 𝑅. (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝑃 = (𝑅 ↾s ∩ (SubDRing‘𝑅))    ⇒   ⊢ (𝑅 ∈ DivRing → 𝑃 ∈ Field)
Theorem	primefld0cl 20739	The prime field contains the zero element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023.)
⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → 0 ∈ ∩ (SubDRing‘𝑅))
Theorem	primefld1cl 20740	The prime field contains the unity element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023.)
⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → 1 ∈ ∩ (SubDRing‘𝑅))
10.4.3  Absolute value (abstract algebra)
Syntax	cabv 20741	The set of absolute values on a ring.
class AbsVal
Definition	df-abv 20742*	Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 15159 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ AbsVal = (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))})
Theorem	abvfval 20743*	Value of the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐴 = {𝑓 ∈ ((0[,)+∞) ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 (((𝑓‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))})
Theorem	isabv 20744*	Elementhood in the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐹 ∈ 𝐴 ↔ (𝐹:𝐵⟶(0[,)+∞) ∧ ∀𝑥 ∈ 𝐵 (((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))))))
Theorem	isabvd 20745*	Properties that determine an absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 4-Dec-2014.)
⊢ (𝜑 → 𝐴 = (AbsVal‘𝑅))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 0 = (0g‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹:𝐵⟶ℝ)    &   ⊢ (𝜑 → (𝐹‘ 0 ) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) → 0 < (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐴)
Theorem	abvrcl 20746	Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝑅 ∈ Ring)
Theorem	abvfge0 20747	An absolute value is a function from the ring to the nonnegative real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹:𝐵⟶(0[,)+∞))
Theorem	abvf 20748	An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹:𝐵⟶ℝ)
Theorem	abvcl 20749	An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ ℝ)
Theorem	abvge0 20750	The absolute value of a number is greater than or equal to zero. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → 0 ≤ (𝐹‘𝑋))
Theorem	abveq0 20751	The value of an absolute value is zero iff the argument is zero. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ((𝐹‘𝑋) = 0 ↔ 𝑋 = 0 ))
Theorem	abvne0 20752	The absolute value of a nonzero number is nonzero. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐹‘𝑋) ≠ 0)
Theorem	abvgt0 20753	The absolute value of a nonzero number is strictly positive. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 0 < (𝐹‘𝑋))
Theorem	abvmul 20754	An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) · (𝐹‘𝑌)))
Theorem	abvtri 20755	An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌)))
Theorem	abv0 20756	The absolute value of zero is zero. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐴 → (𝐹‘ 0 ) = 0)
Theorem	abv1z 20757	The absolute value of one is one in a non-trivial ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → (𝐹‘ 1 ) = 1)
Theorem	abv1 20758	The absolute value of one is one in a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) → (𝐹‘ 1 ) = 1)
Theorem	abvneg 20759	The absolute value of a negative is the same as that of the positive. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁‘𝑋)) = (𝐹‘𝑋))
Theorem	abvsubtri 20760	An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ − = (-g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 − 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌)))
Theorem	abvrec 20761	The absolute value distributes under reciprocal. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 )) → (𝐹‘(𝐼‘𝑋)) = (1 / (𝐹‘𝑋)))
Theorem	abvdiv 20762	The absolute value distributes under division. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝐹‘(𝑋 / 𝑌)) = ((𝐹‘𝑋) / (𝐹‘𝑌)))
Theorem	abvdom 20763	Any ring with an absolute value is a domain, which is to say that it contains no zero divisors. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝑋 · 𝑌) ≠ 0 )
Theorem	abvres 20764	The restriction of an absolute value to a subring is an absolute value. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝑆 = (𝑅 ↾s 𝐶)    &   ⊢ 𝐵 = (AbsVal‘𝑆)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → (𝐹 ↾ 𝐶) ∈ 𝐵)
Theorem	abvtrivd 20765*	The trivial absolute value. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1))    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝑦 · 𝑧) ≠ 0 )    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐴)
Theorem	abvtrivg 20766*	The trivial absolute value. This theorem is not true for rings with zero divisors, which violate the multiplication axiom; abvdom 20763 is the converse of this theorem. (Contributed by SN, 25-Jun-2025.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1))    ⇒   ⊢ (𝑅 ∈ Domn → 𝐹 ∈ 𝐴)
Theorem	abvtriv 20767*	The trivial absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1))    ⇒   ⊢ (𝑅 ∈ DivRing → 𝐹 ∈ 𝐴)
Theorem	abvpropd 20768*	If two structures have the same ring components, they have the same collection of absolute values. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿))
Theorem	abvn0b 20769	Another characterization of domains, hinted at in abvtrivg 20766: a nonzero ring is a domain iff it has an absolute value. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ 𝐴 = (AbsVal‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅))
10.4.4  Star rings
Syntax	cstf 20770	Extend class notation with the functionalization of the *-ring involution.
class *rf
Syntax	csr 20771	Extend class notation with class of all *-rings.
class *-Ring
Definition	df-staf 20772*	Define the functionalization of the involution in a star ring. This is not strictly necessary but by having *𝑟 as an actual function we can state the principal properties of an involution much more cleanly. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ *rf = (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟‘𝑓)‘𝑥)))
Definition	df-srng 20773*	Define class of all star rings. A star ring is a ring with an involution (conjugation) function. Involution (unlike say the ring zero) is not unique and therefore must be added as a new component to the ring. For example, two possible involutions for complex numbers are the identity function and complex conjugation. Definition of involution in [Holland95] p. 204. (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2015.)
⊢ *-Ring = {𝑓 ∣ [(*rf‘𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr‘𝑓)) ∧ 𝑖 = ◡𝑖)}
Theorem	staffval 20774*	The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ ∙ = (*rf‘𝑅)    ⇒   ⊢ ∙ = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥))
Theorem	stafval 20775	The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ ∙ = (*rf‘𝑅)    ⇒   ⊢ (𝐴 ∈ 𝐵 → ( ∙ ‘𝐴) = ( ∗ ‘𝐴))
Theorem	staffn 20776	The functionalization is equal to the original function, if it is a function on the right base set. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ ∙ = (*rf‘𝑅)    ⇒   ⊢ ( ∗ Fn 𝐵 → ∙ = ∗ )
Theorem	issrng 20777	The predicate "is a star ring". (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∗ = (*rf‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring ↔ ( ∗ ∈ (𝑅 RingHom 𝑂) ∧ ∗ = ◡ ∗ ))
Theorem	srngrhm 20778	The involution function in a star ring is an antiautomorphism. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑂 = (oppr‘𝑅)    &   ⊢ ∗ = (*rf‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ∗ ∈ (𝑅 RingHom 𝑂))
Theorem	srngring 20779	A star ring is a ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ (𝑅 ∈ *-Ring → 𝑅 ∈ Ring)
Theorem	srngcnv 20780	The involution function in a star ring is its own inverse function. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*rf‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ∗ = ◡ ∗ )
Theorem	srngf1o 20781	The involution function in a star ring is a bijection. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*rf‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ∗ :𝐵–1-1-onto→𝐵)
Theorem	srngcl 20782	The involution function in a star ring is closed in the ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵) → ( ∗ ‘𝑋) ∈ 𝐵)
Theorem	srngnvl 20783	The involution function in a star ring is an involution. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵) → ( ∗ ‘( ∗ ‘𝑋)) = 𝑋)
Theorem	srngadd 20784	The involution function in a star ring distributes over addition. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ∗ ‘(𝑋 + 𝑌)) = (( ∗ ‘𝑋) + ( ∗ ‘𝑌)))
Theorem	srngmul 20785	The involution function in a star ring distributes over multiplication, with a change in the order of the factors. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ∗ ‘(𝑋 · 𝑌)) = (( ∗ ‘𝑌) · ( ∗ ‘𝑋)))
Theorem	srng1 20786	The conjugate of the ring identity is the identity. (This is sometimes taken as an axiom, and indeed the proof here follows because we defined *𝑟 to be a ring homomorphism, which preserves 1; nevertheless, it is redundant, as can be seen from the proof of issrngd 20788.) (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ( ∗ ‘ 1 ) = 1 )
Theorem	srng0 20787	The conjugate of the ring zero is zero. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ *-Ring → ( ∗ ‘ 0 ) = 0 )
Theorem	issrngd 20788*	Properties that determine a star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2015.)
⊢ (𝜑 → 𝐾 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → ∗ = (*𝑟‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ( ∗ ‘𝑥) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 + 𝑦)) = (( ∗ ‘𝑥) + ( ∗ ‘𝑦)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 · 𝑦)) = (( ∗ ‘𝑦) · ( ∗ ‘𝑥)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ( ∗ ‘( ∗ ‘𝑥)) = 𝑥)    ⇒   ⊢ (𝜑 → 𝑅 ∈ *-Ring)
Theorem	idsrngd 20789*	A commutative ring is a star ring when the conjugate operation is the identity. (Contributed by Thierry Arnoux, 19-Apr-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∗ = (*𝑟‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( ∗ ‘𝑥) = 𝑥)    ⇒   ⊢ (𝜑 → 𝑅 ∈ *-Ring)
10.4.5  Totally ordered rings and fields
Syntax	corng 20790	Extend class notation with the class of all ordered rings.
class oRing
Syntax	cofld 20791	Extend class notation with the class of all ordered fields.
class oField
Definition	df-orng 20792*	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 20793	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 20794*	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 20795	An ordered ring is a ring. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Ring)
Theorem	orngogrp 20796	An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oGrp)
Theorem	isofld 20797	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 20798	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 20799	In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 0 ≤ (𝑋 · 𝑋))
Theorem	ornglmulle 20800	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 ≤ 𝑍)    ⇒   ⊢ (𝜑 → (𝑍 · 𝑋) ≤ (𝑍 · 𝑌))