P. 207 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20601-20700   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cdomn 20601	Class of (ring theoretic) domains.
class Domn
Syntax	cidom 20602	Class of integral domains.
class IDomn
Definition	df-rlreg 20603*	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 20604*	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 20605	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ IDomn = (CRing ∩ Domn)
Theorem	rrgval 20606*	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 20607*	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 20608	Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 ))
Theorem	rrgeq0 20609	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 20610	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 20611	Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝐸 ⊆ 𝐵
Theorem	unitrrg 20612	Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑈 ⊆ 𝐸)
Theorem	rrgnz 20613	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 20614*	Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
Theorem	domnnzr 20615	A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing)
Theorem	domnring 20616	A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring)
Theorem	domneq0 20617	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 20618	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 20619*	The equivalence between the right conjuncts in the right hand sides of isdomn 20614 and isdomn2 20620, in predicate calculus form. (Contributed by SN, 16-Sep-2024.)
⊢ (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → (𝑎 = 0 ∨ 𝑏 = 0 )) ↔ ∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → 𝑏 = 0 ))
Theorem	isdomn2 20620	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 20621	Obsolete version of isdomn2 20620 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 20622	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 20623	A ring is a domain iff the regular elements are the nonzero elements. Compare isdomn2 20620, domnrrg 20622. (Contributed by Thierry Arnoux, 6-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ (𝐵 ∖ { 0 }) = 𝐸))
Theorem	isdomn3 20624	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 20625*	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 20626	A class is a domain if and only if its opposite is a domain, biconditional form of opprdomn 20627. (Contributed by SN, 15-Jun-2015.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ 𝑂 ∈ Domn)
Theorem	opprdomn 20627	The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn → 𝑂 ∈ Domn)
Theorem	isdomn4r 20628*	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 20629	Left-cancellation law for domains, biconditional version of domnlcan 20630. (Contributed by Thierry Arnoux, 8-Jun-2025.) Shorten this theorem and domnlcan 20630 overall. (Revised by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = (𝑋 · 𝑍) ↔ 𝑌 = 𝑍))
Theorem	domnlcan 20630	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 20631	Right-cancellation law for domains, biconditional version of domnrcan 20632. (Contributed by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑍) = (𝑌 · 𝑍) ↔ 𝑋 = 𝑌))
Theorem	domnrcan 20632	Right-cancellation law for domains. (Contributed by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	domneq0r 20633	Right multiplication by a nonzero element does not change zeroness in a domain. Compare rrgeq0 20609. (Contributed by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ 𝑋 = 0 ))
Theorem	isidom 20634	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
Theorem	idomdomd 20635	An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Domn)
Theorem	idomcringd 20636	An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) Formerly subproof of idomringd 20637. (Proof shortened by SN, 14-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
Theorem	idomringd 20637	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 20638	Extend class notation with class of all division rings.
class DivRing
Syntax	cfield 20639	Class of fields.
class Field
Definition	df-drng 20640	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 20641	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ Field = (DivRing ∩ CRing)
Theorem	isdrng 20642	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 20643	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 20644	The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑅 ∈ DivRing    ⇒   ⊢ (𝐵 ∖ { 0 }) = (Unit‘𝑅)
Theorem	drngring 20645	A division ring is a ring. (Contributed by NM, 8-Sep-2011.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
Theorem	drngringd 20646	A division ring is a ring. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Ring)
Theorem	drnggrpd 20647	A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Grp)
Theorem	drnggrp 20648	A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Grp)
Theorem	isfld 20649	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
Theorem	flddrngd 20650	A field is a division ring. (Contributed by SN, 17-Jan-2025.)
⊢ (𝜑 → 𝑅 ∈ Field)    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	fldcrngd 20651	A field is a commutative ring. (Contributed by SN, 23-Nov-2024.)
⊢ (𝜑 → 𝑅 ∈ Field)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
Theorem	isdrng2 20652	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 20653	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 20654	A division ring contains a multiplicative group. (Contributed by NM, 8-Sep-2011.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝑅 ∈ DivRing → 𝐺 ∈ Grp)
Theorem	drngid 20655	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 20656	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 20657	A division ring is a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
Theorem	drngdomn 20658	A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Domn)
Theorem	drngmcl 20659	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 20660	Obsolete version of drngmcl 20659 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 20661	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 20662	Closure of the multiplicative inverse in a division ring. (reccl 11844 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ∈ 𝐵)
Theorem	drnginvrn0 20663	The multiplicative inverse in a division ring is nonzero. (recne0 11850 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ≠ 0 )
Theorem	drnginvrcld 20664	Closure of the multiplicative inverse in a division ring. (reccld 11951 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ 𝐵)
Theorem	drnginvrl 20665	Property of the multiplicative inverse in a division ring. (recid2 11852 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ((𝐼‘𝑋) · 𝑋) = 1 )
Theorem	drnginvrr 20666	Property of the multiplicative inverse in a division ring. (recid 11851 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝑋 · (𝐼‘𝑋)) = 1 )
Theorem	drnginvrld 20667	Property of the multiplicative inverse in a division ring. (recid2d 11954 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → ((𝐼‘𝑋) · 𝑋) = 1 )
Theorem	drnginvrrd 20668	Property of the multiplicative inverse in a division ring. (recidd 11953 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 · (𝐼‘𝑋)) = 1 )
Theorem	drngmul0or 20669	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 20670	Obsolete version of drngmul0or 20669 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 20671	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 20672	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 20673	The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing ↔ 𝑂 ∈ DivRing)
Theorem	isdrngd 20674*	Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element 𝑥 should have a left-inverse 𝐼(𝑥). See isdrngrd 20675 for the characterization using right-inverses. (Contributed by NM, 2-Aug-2013.) Remove hypothesis. (Revised by SN, 19-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 0 = (0g‘𝑅))    &   ⊢ (𝜑 → 1 = (1r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 )    &   ⊢ (𝜑 → 1 ≠ 0 )    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝐼 · 𝑥) = 1 )    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	isdrngrd 20675*	Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element 𝑥 should have a right-inverse 𝐼(𝑥). See isdrngd 20674 for the characterization using left-inverses. (Contributed by NM, 10-Aug-2013.) Remove hypothesis. (Revised by SN, 19-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → · = (.r‘𝑅))    &   ⊢ (𝜑 → 0 = (0g‘𝑅))    &   ⊢ (𝜑 → 1 = (1r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 )    &   ⊢ (𝜑 → 1 ≠ 0 )    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝑥 · 𝐼) = 1 )    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	isdrngdOLD 20676*	Obsolete version of isdrngd 20674 as of 19-Feb-2025. (Contributed by NM, 2-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	isdrngrdOLD 20677*	Obsolete version of isdrngrd 20675 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 20678*	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 20679*	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 20680	A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof shortened by SN, 11-Nov-2024.)
⊢ (𝑅 ∈ Field → 𝑅 ∈ IDomn)
Theorem	fidomndrnglem 20681*	Lemma for fidomndrng 20682. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ { 0 }))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝐴))    ⇒   ⊢ (𝜑 → 𝐴 ∥ 1 )
Theorem	fidomndrng 20682	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 20683	A finite integral domain is a field. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐵 ∈ Fin → (𝑅 ∈ IDomn ↔ 𝑅 ∈ Field))
Theorem	rng1nnzr 20684	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 20685	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 20686	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 20687	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 20688	The zero ring is not a field. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    ⇒   ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∉ Field)
Theorem	issubdrg 20689*	Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → (𝑆 ∈ DivRing ↔ ∀𝑥 ∈ (𝐴 ∖ { 0 })(𝐼‘𝑥) ∈ 𝐴))
Theorem	drhmsubc 20690*	According to df-subc 17774, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17802 and subcss2 17805). 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 20691*	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 20692*	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 20693*	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 20694*	According to df-subc 17774, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17802 and subcss2 17805). 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 20695	Syntax for subfields (sub-division-rings).
class SubDRing
Definition	df-sdrg 20696*	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 20707), 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 20697	Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.)
⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing))
Theorem	sdrgrcl 20698	Reverse closure for a sub-division-ring predicate. (Contributed by SN, 19-Feb-2025.)
⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝑅 ∈ DivRing)
Theorem	sdrgdrng 20699	A sub-division-ring is a division ring. (Contributed by SN, 19-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝑆 ∈ DivRing)
Theorem	sdrgsubrg 20700	A sub-division-ring is a subring. (Contributed by SN, 19-Feb-2025.)
⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝐴 ∈ (SubRing‘𝑅))