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	rrgsupp 20701	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 20702	Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝐸 ⊆ 𝐵
Theorem	unitrrg 20703	Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑈 ⊆ 𝐸)
Theorem	rrgnz 20704	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 20705*	Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
Theorem	domnnzr 20706	A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing)
Theorem	domnring 20707	A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring)
Theorem	domneq0 20708	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 20709	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 20710*	The equivalence between the right conjuncts in the right hand sides of isdomn 20705 and isdomn2 20711, in predicate calculus form. (Contributed by SN, 16-Sep-2024.)
⊢ (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → (𝑎 = 0 ∨ 𝑏 = 0 )) ↔ ∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → 𝑏 = 0 ))
Theorem	isdomn2 20711	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 20712	Obsolete version of isdomn2 20711 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 20713	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 20714	A ring is a domain iff the regular elements are the nonzero elements. Compare isdomn2 20711, domnrrg 20713. (Contributed by Thierry Arnoux, 6-May-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ (𝐵 ∖ { 0 }) = 𝐸))
Theorem	isdomn3 20715	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 20716*	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 20717	A class is a domain if and only if its opposite is a domain, biconditional form of opprdomn 20718. (Contributed by SN, 15-Jun-2015.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ 𝑂 ∈ Domn)
Theorem	opprdomn 20718	The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn → 𝑂 ∈ Domn)
Theorem	isdomn4r 20719*	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 20720	Left-cancellation law for domains, biconditional version of domnlcan 20721. (Contributed by Thierry Arnoux, 8-Jun-2025.) Shorten this theorem and domnlcan 20721 overall. (Revised by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = (𝑋 · 𝑍) ↔ 𝑌 = 𝑍))
Theorem	domnlcan 20721	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 20722	Right-cancellation law for domains, biconditional version of domnrcan 20723. (Contributed by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑍) = (𝑌 · 𝑍) ↔ 𝑋 = 𝑌))
Theorem	domnrcan 20723	Right-cancellation law for domains. (Contributed by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	domneq0r 20724	Right multiplication by a nonzero element does not change zeroness in a domain. Compare rrgeq0 20700. (Contributed by SN, 21-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ 𝑋 = 0 ))
Theorem	isidom 20725	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
Theorem	idomdomd 20726	An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Domn)
Theorem	idomcringd 20727	An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) Formerly subproof of idomringd 20728. (Proof shortened by SN, 14-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
Theorem	idomringd 20728	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 20729	Extend class notation with class of all division rings.
class DivRing
Syntax	cfield 20730	Class of fields.
class Field
Definition	df-drng 20731	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 20732	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ Field = (DivRing ∩ CRing)
Theorem	isdrng 20733	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 20734	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 20735	The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑅 ∈ DivRing    ⇒   ⊢ (𝐵 ∖ { 0 }) = (Unit‘𝑅)
Theorem	drngring 20736	A division ring is a ring. (Contributed by NM, 8-Sep-2011.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
Theorem	drngringd 20737	A division ring is a ring. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Ring)
Theorem	drnggrpd 20738	A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Grp)
Theorem	drnggrp 20739	A division ring is a group (closed form). (Contributed by NM, 8-Sep-2011.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Grp)
Theorem	isfld 20740	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
Theorem	flddrngd 20741	A field is a division ring. (Contributed by SN, 17-Jan-2025.)
⊢ (𝜑 → 𝑅 ∈ Field)    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	fldcrngd 20742	A field is a commutative ring. (Contributed by SN, 23-Nov-2024.)
⊢ (𝜑 → 𝑅 ∈ Field)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
Theorem	isdrng2 20743	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 20744	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 20745	A division ring contains a multiplicative group. (Contributed by NM, 8-Sep-2011.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝑅 ∈ DivRing → 𝐺 ∈ Grp)
Theorem	drngid 20746	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 20747	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 20748	A division ring is a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
Theorem	drngdomn 20749	A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015.)
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Domn)
Theorem	drngmcl 20750	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 20751	Obsolete version of drngmcl 20750 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 20752	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 20753	Closure of the multiplicative inverse in a division ring. (reccl 11929 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ∈ 𝐵)
Theorem	drnginvrn0 20754	The multiplicative inverse in a division ring is nonzero. (recne0 11935 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ≠ 0 )
Theorem	drnginvrcld 20755	Closure of the multiplicative inverse in a division ring. (reccld 12036 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ 𝐵)
Theorem	drnginvrl 20756	Property of the multiplicative inverse in a division ring. (recid2 11937 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ((𝐼‘𝑋) · 𝑋) = 1 )
Theorem	drnginvrr 20757	Property of the multiplicative inverse in a division ring. (recid 11936 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝑋 · (𝐼‘𝑋)) = 1 )
Theorem	drnginvrld 20758	Property of the multiplicative inverse in a division ring. (recid2d 12039 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → ((𝐼‘𝑋) · 𝑋) = 1 )
Theorem	drnginvrrd 20759	Property of the multiplicative inverse in a division ring. (recidd 12038 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 · (𝐼‘𝑋)) = 1 )
Theorem	drngmul0or 20760	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 20761	Obsolete version of drngmul0or 20760 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 20762	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 20763	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 20764	The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing ↔ 𝑂 ∈ DivRing)
Theorem	isdrngd 20765*	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 20766 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 20766*	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 20765 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 20767*	Obsolete version of isdrngd 20765 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 20768*	Obsolete version of isdrngrd 20766 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 20769*	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 20770*	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 20771	A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof shortened by SN, 11-Nov-2024.)
⊢ (𝑅 ∈ Field → 𝑅 ∈ IDomn)
Theorem	fldidomOLD 20772	Obsolete version of fldidom 20771 as of 11-Nov-2024. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑅 ∈ Field → 𝑅 ∈ IDomn)
Theorem	fidomndrnglem 20773*	Lemma for fidomndrng 20774. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ { 0 }))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝐴))    ⇒   ⊢ (𝜑 → 𝐴 ∥ 1 )
Theorem	fidomndrng 20774	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 20775	A finite integral domain is a field. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐵 ∈ Fin → (𝑅 ∈ IDomn ↔ 𝑅 ∈ Field))
Theorem	rng1nnzr 20776	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 20777	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 20778	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 20779	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 20780	The zero ring is not a field. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    ⇒   ⊢ (𝑍 ∈ 𝑉 → 𝑀 ∉ Field)
Theorem	issubdrg 20781*	Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → (𝑆 ∈ DivRing ↔ ∀𝑥 ∈ (𝐴 ∖ { 0 })(𝐼‘𝑥) ∈ 𝐴))
Theorem	drhmsubc 20782*	According to df-subc 17856, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17885 and subcss2 17888). 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 20783*	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 20784*	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 20785*	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 20786*	According to df-subc 17856, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17885 and subcss2 17888). 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 20787	Syntax for subfields (sub-division-rings).
class SubDRing
Definition	df-sdrg 20788*	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 20799), 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 20789	Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.)
⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing))
Theorem	sdrgrcl 20790	Reverse closure for a sub-division-ring predicate. (Contributed by SN, 19-Feb-2025.)
⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝑅 ∈ DivRing)
Theorem	sdrgdrng 20791	A sub-division-ring is a division ring. (Contributed by SN, 19-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝑆 ∈ DivRing)
Theorem	sdrgsubrg 20792	A sub-division-ring is a subring. (Contributed by SN, 19-Feb-2025.)
⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝐴 ∈ (SubRing‘𝑅))
Theorem	sdrgid 20793	Every division ring is a division subring of itself. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ DivRing → 𝐵 ∈ (SubDRing‘𝑅))
Theorem	sdrgss 20794	A division subring is a subset of the base set. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑆 ∈ (SubDRing‘𝑅) → 𝑆 ⊆ 𝐵)
Theorem	sdrgbas 20795	Base set of a sub-division-ring structure. (Contributed by SN, 19-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubDRing‘𝑅) → 𝐴 = (Base‘𝑆))
Theorem	issdrg2 20796*	Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑆 ∖ { 0 })(𝐼‘𝑥) ∈ 𝑆))
Theorem	sdrgunit 20797	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 20798	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 20799	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 20800*	Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))