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	rhmsscrnghm 20701	The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the non-unital ring homomorphisms between non-unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝑆 = (Rng ∩ 𝑈))    ⇒   ⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) ⊆cat ( RngHom ↾ (𝑆 × 𝑆)))
Theorem	rhmsubcrngclem1 20702	Lemma 1 for rhmsubcrngc 20704. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rhmsubcrngclem2 20703*	Lemma 2 for rhmsubcrngc 20704. (Contributed by AV, 12-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rhmsubcrngc 20704	The unital ring homomorphisms between unital rings (in a universe) are a subcategory of the category of non-unital rings. (Contributed by AV, 12-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶))
Theorem	rngcresringcat 20705	The restriction of the category of non-unital rings to the set of unital ring homomorphisms is the category of unital rings. (Contributed by AV, 16-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → (𝐶 ↾cat 𝐻) = (RingCat‘𝑈))
Theorem	ringcsect 20706	A section in the category of unital rings, written out. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐸 = (Base‘𝑋)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸))))
Theorem	ringcinv 20707	An inverse in the category of unital rings is the converse operation. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑁 = (Inv‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)))
Theorem	ringciso 20708	An isomorphism in the category of unital rings is a bijection. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RingIso 𝑌)))
Theorem	ringcbasbas 20709	An element of the base set of the base set of the category of unital rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    ⇒   ⊢ ((𝜑 ∧ 𝑅 ∈ 𝐵) → (Base‘𝑅) ∈ 𝑈)
Theorem	funcringcsetc 20710*	The "natural forgetful functor" from the category of unital rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 26-Mar-2020.)
⊢ 𝑅 = (RingCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	zrtermoringc 20711	The zero ring is a terminal object in the category of unital rings. (Contributed by AV, 17-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑍 ∈ (TermO‘𝐶))
Theorem	zrninitoringc 20712*	The zero ring is not an initial object in the category of unital rings (if the universe contains at least one unital ring different from the zero ring). (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → ∃𝑟 ∈ (Base‘𝐶)𝑟 ∈ NzRing)    ⇒   ⊢ (𝜑 → 𝑍 ∉ (InitO‘𝐶))
10.3.14.3  Subcategories of the category of rings
Theorem	srhmsubclem1 20713*	Lemma 1 for srhmsubc 20716. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    ⇒   ⊢ (𝑋 ∈ 𝐶 → 𝑋 ∈ (𝑈 ∩ Ring))
Theorem	srhmsubclem2 20714*	Lemma 2 for srhmsubc 20716. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    ⇒   ⊢ ((𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ (Base‘(RingCat‘𝑈)))
Theorem	srhmsubclem3 20715*	Lemma 3 for srhmsubc 20716. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ ((𝑈 ∈ 𝑉 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐽𝑌) = (𝑋(Hom ‘(RingCat‘𝑈))𝑌))
Theorem	srhmsubc 20716*	According to df-subc 17835, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17863 and subcss2 17866). Therefore, the set of special ring homomorphisms (i.e., ring homomorphisms from a special ring to another ring of that kind) is a subcategory of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈ (Subcat‘(RingCat‘𝑈)))
Theorem	sringcat 20717*	The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCat‘𝑈) ↾cat 𝐽) ∈ Cat)
Theorem	crhmsubc 20718*	According to df-subc 17835, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17863 and subcss2 17866). Therefore, the set of commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ CRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈ (Subcat‘(RingCat‘𝑈)))
Theorem	cringcat 20719*	The restriction of the category of (unital) rings to the set of commutative ring homomorphisms is a category, the "category of commutative rings". (Contributed by AV, 19-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ CRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCat‘𝑈) ↾cat 𝐽) ∈ Cat)
Theorem	rngcrescrhm 20720	The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → (𝐶 ↾cat 𝐻) = ((𝐶 ↾s 𝑅) sSet ⟨(Hom ‘ndx), 𝐻⟩))
Theorem	rhmsubclem1 20721	Lemma 1 for rhmsubc 20725. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝑅 × 𝑅))
Theorem	rhmsubclem2 20722	Lemma 2 for rhmsubc 20725. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌))
Theorem	rhmsubclem3 20723*	Lemma 3 for rhmsubc 20725. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((Id‘(RngCat‘𝑈))‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rhmsubclem4 20724*	Lemma 4 for rhmsubc 20725. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(RngCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rhmsubc 20725	According to df-subc 17835, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17863 and subcss2 17866). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘(RngCat‘𝑈)))
Theorem	rhmsubccat 20726	The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → ((RngCat‘𝑈) ↾cat 𝐻) ∈ Cat)
10.3.15  Left regular elements and domains
Syntax	crlreg 20727	Set of left-regular elements in a ring.
class RLReg
Syntax	cdomn 20728	Class of (ring theoretic) domains.
class Domn
Syntax	cidom 20729	Class of integral domains.
class IDomn
Definition	df-rlreg 20730*	Define the set of left-regular elements in a ring as those elements which are not left zero divisors, meaning that multiplying a nonzero element on the left by a left-regular element gives a nonzero product. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ RLReg = (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))})
Definition	df-domn 20731*	A domain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ Domn = {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))}
Definition	df-idom 20732	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ IDomn = (CRing ∩ Domn)
Theorem	rrgval 20733*	Value of the set or left-regular elements in a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → 𝑦 = 0 )}
Theorem	isrrg 20734*	Membership in the set of left-regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ((𝑋 · 𝑦) = 0 → 𝑦 = 0 )))
Theorem	rrgeq0i 20735	Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 ))
Theorem	rrgeq0 20736	Left-multiplication by a left regular element does not change zeroness. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 ↔ 𝑌 = 0 ))
Theorem	rrgsupp 20737	Left multiplication by a left regular element does not change the support set of a vector. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Revised by AV, 20-Jul-2019.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    &   ⊢ (𝜑 → 𝑌:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 × {𝑋}) ∘f · 𝑌) supp 0 ) = (𝑌 supp 0 ))
Theorem	rrgss 20738	Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝐸 ⊆ 𝐵
Theorem	unitrrg 20739	Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑈 ⊆ 𝐸)
Theorem	rrgnz 20740	In a nonzero ring, the zero is a left zero divisor (that is, not a left-regular element). (Contributed by Thierry Arnoux, 6-May-2025.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing → ¬ 0 ∈ 𝐸)
Theorem	isdomn 20741*	Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
Theorem	domnnzr 20742	A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing)
Theorem	domnring 20743	A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring)
Theorem	domneq0 20744	In a domain, a product is zero iff it has a zero factor. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 ↔ (𝑋 = 0 ∨ 𝑌 = 0 )))
Theorem	domnmuln0 20745	In a domain, a product of nonzero elements is nonzero. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Domn ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝑋 · 𝑌) ≠ 0 )
Theorem	isdomn5 20746*	The equivalence between the right conjuncts in the right hand sides of isdomn 20741 and isdomn2 20747, in predicate calculus form. (Contributed by SN, 16-Sep-2024.)
⊢ (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → (𝑎 = 0 ∨ 𝑏 = 0 )) ↔ ∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → 𝑏 = 0 ))
Theorem	isdomn2 20747	A ring is a domain iff all nonzero elements are regular elements. (Contributed by Mario Carneiro, 28-Mar-2015.) (Proof shortened by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ (𝐵 ∖ { 0 }) ⊆ 𝐸))
Theorem	isdomn2OLD 20748	Obsolete version of isdomn2 20747 as of 21-Jun-2025. (Contributed by Mario Carneiro, 28-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ (𝐵 ∖ { 0 }) ⊆ 𝐸))
Theorem	domnrrg 20749	In a domain, a nonzero element is a regular element. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝐸)
Theorem	isdomn6 20750	A ring is a domain iff the regular elements are the nonzero elements. Compare isdomn2 20747, domnrrg 20749. (Contributed by Thierry Arnoux, 6-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ (𝐵 ∖ { 0 }) = 𝐸))
Theorem	isdomn3 20751	Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈ (SubMnd‘𝑈)))
Theorem	isdomn4 20752*	A ring is a domain iff it is nonzero and the left cancellation law for multiplication holds. (Contributed by SN, 15-Sep-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐)))
Theorem	opprdomnb 20753	A class is a domain if and only if its opposite is a domain, biconditional form of opprdomn 20754. (Contributed by SN, 15-Jun-2015.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ 𝑂 ∈ Domn)
Theorem	opprdomn 20754	The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn → 𝑂 ∈ Domn)
Theorem	isdomn4r 20755*	A ring is a domain iff it is nonzero and the right cancellation law for multiplication holds. (Contributed by SN, 20-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ (𝐵 ∖ { 0 })((𝑎 · 𝑐) = (𝑏 · 𝑐) → 𝑎 = 𝑏)))
Theorem	domnlcanb 20756	Left-cancellation law for domains, biconditional version of domnlcan 20757. (Contributed by Thierry Arnoux, 8-Jun-2025.) Shorten this theorem and domnlcan 20757 overall. (Revised by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = (𝑋 · 𝑍) ↔ 𝑌 = 𝑍))
Theorem	domnlcan 20757	Left-cancellation law for domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) (Proof shortened by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 · 𝑍))    ⇒   ⊢ (𝜑 → 𝑌 = 𝑍)
Theorem	domnrcanb 20758	Right-cancellation law for domains, biconditional version of domnrcan 20759. (Contributed by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑍) = (𝑌 · 𝑍) ↔ 𝑋 = 𝑌))
Theorem	domnrcan 20759	Right-cancellation law for domains. (Contributed by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	domneq0r 20760	Right multiplication by a nonzero element does not change zeroness in a domain. Compare rrgeq0 20736. (Contributed by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ 𝑋 = 0 ))
Theorem	isidom 20761	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
Theorem	idomdomd 20762	An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Domn)
Theorem	idomcringd 20763	An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) Formerly subproof of idomringd 20764. (Proof shortened by SN, 14-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
Theorem	idomringd 20764	An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Ring)
10.4  Division rings and fields
10.4.1  Definition and basic properties
Syntax	cdr 20765	Extend class notation with class of all division rings.
class DivRing
Syntax	cfield 20766	Class of fields.
class Field
Definition	df-drng 20767	Define class of all division rings. A division ring is a ring in which the set of units is exactly the nonzero elements of the ring. (Contributed by NM, 18-Oct-2012.)
⊢ DivRing = {𝑟 ∈ Ring ∣ (Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g‘𝑟)})}
Definition	df-field 20768	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ Field = (DivRing ∩ CRing)
Theorem	isdrng 20769	The predicate "is a division ring". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
Theorem	drngunit 20770	Elementhood in the set of units when 𝑅 is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 )))
Theorem	drngui 20771	The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑅 ∈ DivRing    ⇒   ⊢ (𝐵 ∖ { 0 }) = (Unit‘𝑅)
Theorem	drngring 20772	A division ring is a ring. (Contributed by NM, 8-Sep-2011.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
Theorem	drngringd 20773	A division ring is a ring. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Ring)
Theorem	drnggrpd 20774	A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Grp)
Theorem	drnggrp 20775	A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Grp)
Theorem	isfld 20776	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
Theorem	flddrngd 20777	A field is a division ring. (Contributed by SN, 17-Jan-2025.)
⊢ (𝜑 → 𝑅 ∈ Field)    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	fldcrngd 20778	A field is a commutative ring. (Contributed by SN, 23-Nov-2024.)
⊢ (𝜑 → 𝑅 ∈ Field)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
Theorem	isdrng2 20779	A division ring can equivalently be defined as a ring such that the nonzero elements form a group under multiplication (from which it follows that this is the same group as the group of units). (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ Grp))
Theorem	drngprop 20780	If two structures have the same ring components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Mario Carneiro, 28-Dec-2014.)
⊢ (Base‘𝐾) = (Base‘𝐿)    &   ⊢ (+g‘𝐾) = (+g‘𝐿)    &   ⊢ (.r‘𝐾) = (.r‘𝐿)    ⇒   ⊢ (𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing)
Theorem	drngmgp 20781	A division ring contains a multiplicative group. (Contributed by NM, 8-Sep-2011.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝑅 ∈ DivRing → 𝐺 ∈ Grp)
Theorem	drngid 20782	A division ring's unity is the identity element of its multiplicative group. (Contributed by NM, 7-Sep-2011.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝑅 ∈ DivRing → 1 = (0g‘𝐺))
Theorem	drngunz 20783	A division ring's unity is different from its zero. (Contributed by NM, 8-Sep-2011.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → 1 ≠ 0 )
Theorem	drngnzr 20784	A division ring is a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
Theorem	drngdomn 20785	A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Domn)
Theorem	drngmcl 20786	The product of two nonzero elements of a division ring is nonzero. (Contributed by NM, 7-Sep-2011.) (Proof shortened by SN, 25-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ (𝐵 ∖ { 0 }) ∧ 𝑌 ∈ (𝐵 ∖ { 0 })) → (𝑋 · 𝑌) ∈ (𝐵 ∖ { 0 }))
Theorem	drngmclOLD 20787	Obsolete version of drngmcl 20786 as of 25-Jun-2025. The product of two nonzero elements of a division ring is nonzero. (Contributed by NM, 7-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ (𝐵 ∖ { 0 }) ∧ 𝑌 ∈ (𝐵 ∖ { 0 })) → (𝑋 · 𝑌) ∈ (𝐵 ∖ { 0 }))
Theorem	drngid2 20788	Properties showing that an element 𝐼 is the identity element of a division ring. (Contributed by Mario Carneiro, 11-Oct-2013.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → ((𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ∧ (𝐼 · 𝐼) = 𝐼) ↔ 1 = 𝐼))
Theorem	drnginvrcl 20789	Closure of the multiplicative inverse in a division ring. (reccl 11845 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ∈ 𝐵)
Theorem	drnginvrn0 20790	The multiplicative inverse in a division ring is nonzero. (recne0 11851 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ≠ 0 )
Theorem	drnginvrcld 20791	Closure of the multiplicative inverse in a division ring. (reccld 11953 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ 𝐵)
Theorem	drnginvrl 20792	Property of the multiplicative inverse in a division ring. (recid2 11853 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ((𝐼‘𝑋) · 𝑋) = 1 )
Theorem	drnginvrr 20793	Property of the multiplicative inverse in a division ring. (recid 11852 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝑋 · (𝐼‘𝑋)) = 1 )
Theorem	drnginvrld 20794	Property of the multiplicative inverse in a division ring. (recid2d 11956 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → ((𝐼‘𝑋) · 𝑋) = 1 )
Theorem	drnginvrrd 20795	Property of the multiplicative inverse in a division ring. (recidd 11955 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 · (𝐼‘𝑋)) = 1 )
Theorem	drngmul0or 20796	A product is zero iff one of its factors is zero. (Contributed by NM, 8-Oct-2014.) (Proof shortened by SN, 25-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ (𝑋 = 0 ∨ 𝑌 = 0 )))
Theorem	drngmul0orOLD 20797	Obsolete version of drngmul0or 20796 as of 25-Jun-2025. (Contributed by NM, 8-Oct-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ (𝑋 = 0 ∨ 𝑌 = 0 )))
Theorem	drngmulne0 20798	A product is nonzero iff both its factors are nonzero. (Contributed by NM, 18-Oct-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) ≠ 0 ↔ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )))
Theorem	drngmuleq0 20799	An element is zero iff its product with a nonzero element is zero. (Contributed by NM, 8-Oct-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ 𝑋 = 0 ))
Theorem	opprdrng 20800	The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing ↔ 𝑂 ∈ DivRing)