P. 145 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14401-14500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rimrhm 14401	A ring isomorphism is a homomorphism. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	rhmfn 14402	The mapping of two rings to the ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.)
⊢ RingHom Fn (Ring × Ring)
Theorem	rhmval 14403	The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.)
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) → (𝑅 RingHom 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))))
Theorem	rhmco 14404	The composition of ring homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐹 ∈ (𝑇 RingHom 𝑈) ∧ 𝐺 ∈ (𝑆 RingHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 RingHom 𝑈))
Theorem	rhmdvdsr 14405	A ring homomorphism preserves the divisibility relation. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ 𝑋 = (Base‘𝑅)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ / = (∥r‘𝑆)    ⇒   ⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ∥ 𝐵) → (𝐹‘𝐴) / (𝐹‘𝐵))
Theorem	rhmopp 14406	A ring homomorphism is also a ring homomorphism for the opposite rings. (Contributed by Thierry Arnoux, 27-Oct-2017.)
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((oppr‘𝑅) RingHom (oppr‘𝑆)))
Theorem	elrhmunit 14407	Ring homomorphisms preserve unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.)
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘𝐴) ∈ (Unit‘𝑆))
Theorem	rhmunitinv 14408	Ring homomorphisms preserve the inverse of unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.)
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘((invr‘𝑅)‘𝐴)) = ((invr‘𝑆)‘(𝐹‘𝐴)))
7.3.9  Nonzero rings and zero rings
Syntax	cnzr 14409	The class of nonzero rings.
class NzRing
Definition	df-nzr 14410	A nonzero or nontrivial ring is a ring with at least two values, or equivalently where 1 and 0 are different. (Contributed by Stefan O'Rear, 24-Feb-2015.)
⊢ NzRing = {𝑟 ∈ Ring ∣ (1r‘𝑟) ≠ (0g‘𝑟)}
Theorem	isnzr 14411	Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 ≠ 0 ))
Theorem	nzrnz 14412	One and zero are different in a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing → 1 ≠ 0 )
Theorem	nzrring 14413	A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof shortened by SN, 23-Feb-2025.)
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring)
Theorem	isnzr2 14414	Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 2o ≼ 𝐵))
Theorem	opprnzrbg 14415	The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 14416. (Contributed by SN, 20-Jun-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ NzRing ↔ 𝑂 ∈ NzRing))
Theorem	opprnzr 14416	The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing → 𝑂 ∈ NzRing)
Theorem	ringelnzr 14417	A ring is nonzero if it has a nonzero element. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Revised by Mario Carneiro, 13-Jun-2015.)
⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (𝐵 ∖ { 0 })) → 𝑅 ∈ NzRing)
Theorem	nzrunit 14418	A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → 𝐴 ≠ 0 )
Theorem	01eq0ring 14419	If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019.) (Proof shortened by SN, 23-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 0 = 1 ) → 𝐵 = { 0 })
7.3.10  Local rings
Syntax	clring 14420	Extend class notation with class of all local rings.
class LRing
Definition	df-lring 14421*	A local ring is a nonzero ring where for any two elements summing to one, at least one is invertible. Any field is a local ring; the ring of integers is an example of a ring which is not a local ring. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.)
⊢ LRing = {𝑟 ∈ NzRing ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑥(+g‘𝑟)𝑦) = (1r‘𝑟) → (𝑥 ∈ (Unit‘𝑟) ∨ 𝑦 ∈ (Unit‘𝑟)))}
Theorem	islring 14422*	The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ LRing ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 1 → (𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈))))
Theorem	lringnzr 14423	A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.)
⊢ (𝑅 ∈ LRing → 𝑅 ∈ NzRing)
Theorem	lringring 14424	A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.)
⊢ (𝑅 ∈ LRing → 𝑅 ∈ Ring)
Theorem	lringnz 14425	A local ring is a nonzero ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.)
⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ LRing → 1 ≠ 0 )
Theorem	lringuplu 14426	If the sum of two elements of a local ring is invertible, then at least one of the summands must be invertible. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ LRing)    &   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈))
Theorem	opprlring 14427	The opposite of a local ring is also a local ring. (Contributed by NM, 18-Oct-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ LRing ↔ 𝑂 ∈ LRing)
7.3.11  Subrings
7.3.11.1  Subrings of non-unital rings
Syntax	csubrng 14428	Extend class notation with all subrings of a non-unital ring.
class SubRng
Definition	df-subrng 14429*	Define a subring of a non-unital ring as a set of elements that is a non-unital ring in its own right. In this section, a subring of a non-unital ring is simply called "subring", unless it causes any ambiguity with SubRing. (Contributed by AV, 14-Feb-2025.)
⊢ SubRng = (𝑤 ∈ Rng ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Rng})
Theorem	issubrng 14430	The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) ↔ (𝑅 ∈ Rng ∧ (𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵))
Theorem	subrngss 14431	A subring is a subset. (Contributed by AV, 14-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝐴 ⊆ 𝐵)
Theorem	subrngid 14432	Every non-unital ring is a subring of itself. (Contributed by AV, 14-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → 𝐵 ∈ (SubRng‘𝑅))
Theorem	subrngrng 14433	A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝑆 ∈ Rng)
Theorem	subrngrcl 14434	Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.)
⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝑅 ∈ Rng)
Theorem	subrngsubg 14435	A subring is a subgroup. (Contributed by AV, 14-Feb-2025.)
⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))
Theorem	subrngringnsg 14436	A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.)
⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝐴 ∈ (NrmSGrp‘𝑅))
Theorem	subrngbas 14437	Base set of a subring structure. (Contributed by AV, 14-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝐴 = (Base‘𝑆))
Theorem	subrng0 14438	A subring always has the same additive identity. (Contributed by AV, 14-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → 0 = (0g‘𝑆))
Theorem	subrngacl 14439	A subring is closed under addition. (Contributed by AV, 14-Feb-2025.)
⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRng‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 + 𝑌) ∈ 𝐴)
Theorem	subrngmcl 14440	A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 14464. (Revised by AV, 14-Feb-2025.)
⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRng‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 · 𝑌) ∈ 𝐴)
Theorem	issubrng2 14441*	Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → (𝐴 ∈ (SubRng‘𝑅) ↔ (𝐴 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)))
Theorem	opprsubrngg 14442	Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (SubRng‘𝑅) = (SubRng‘𝑂))
Theorem	subrngintm 14443*	The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025.)
⊢ ((𝑆 ⊆ (SubRng‘𝑅) ∧ ∃𝑗 𝑗 ∈ 𝑆) → ∩ 𝑆 ∈ (SubRng‘𝑅))
Theorem	subrngin 14444	The intersection of two subrings is a subring. (Contributed by AV, 15-Feb-2025.)
⊢ ((𝐴 ∈ (SubRng‘𝑅) ∧ 𝐵 ∈ (SubRng‘𝑅)) → (𝐴 ∩ 𝐵) ∈ (SubRng‘𝑅))
Theorem	subsubrng 14445	A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → (𝐵 ∈ (SubRng‘𝑆) ↔ (𝐵 ∈ (SubRng‘𝑅) ∧ 𝐵 ⊆ 𝐴)))
Theorem	subsubrng2 14446	The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → (SubRng‘𝑆) = ((SubRng‘𝑅) ∩ 𝒫 𝐴))
Theorem	subrngpropd 14447*	If two structures have the same ring components (properties), they have the same set of subrings. (Contributed by AV, 17-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (SubRng‘𝐾) = (SubRng‘𝐿))
7.3.11.2  Subrings of unital rings
Syntax	csubrg 14448	Extend class notation with all subrings of a ring.
class SubRing
Syntax	crgspn 14449	Extend class notation with span of a set of elements over a ring.
class RingSpan
Definition	df-subrg 14450*	Define a subring of a ring as a set of elements that is a ring in its own right and contains the multiplicative identity. The additional constraint is necessary because the multiplicative identity of a ring, unlike the additive identity of a ring/group or the multiplicative identity of a field, cannot be identified by a local property. Thus, it is possible for a subset of a ring to be a ring while not containing the true identity if it contains a false identity. For instance, the subset (ℤ × {0}) of (ℤ × ℤ) (where multiplication is componentwise) contains the false identity ⟨1, 0⟩ which preserves every element of the subset and thus appears to be the identity of the subset, but is not the identity of the larger ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ SubRing = (𝑤 ∈ Ring ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ((𝑤 ↾s 𝑠) ∈ Ring ∧ (1r‘𝑤) ∈ 𝑠)})
Definition	df-rgspn 14451*	The ring-span of a set of elements in a ring is the smallest subring which contains all of them. (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ RingSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}))
Theorem	issubrg 14452	The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof shortened by AV, 12-Oct-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)))
Theorem	subrgss 14453	A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵)
Theorem	subrgid 14454	Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅))
Theorem	subrgring 14455	A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring)
Theorem	subrgcrng 14456	A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ CRing)
Theorem	subrgrcl 14457	Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
Theorem	subrgsubg 14458	A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))
Theorem	subrg0 14459	A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 0 = (0g‘𝑆))
Theorem	subrg1cl 14460	A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 ∈ 𝐴)
Theorem	subrgbas 14461	Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆))
Theorem	subrg1 14462	A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 = (1r‘𝑆))
Theorem	subrgacl 14463	A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 + 𝑌) ∈ 𝐴)
Theorem	subrgmcl 14464	A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 · 𝑌) ∈ 𝐴)
Theorem	subrgsubm 14465	A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubMnd‘𝑀))
Theorem	subrgdvds 14466	If an element divides another in a subring, then it also divides the other in the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ ∥ = (∥r‘𝑅)    &   ⊢ 𝐸 = (∥r‘𝑆)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐸 ⊆ ∥ )
Theorem	subrguss 14467	A unit of a subring is a unit of the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑉 = (Unit‘𝑆)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ⊆ 𝑈)
Theorem	subrginv 14468	A subring always has the same inversion function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑆)    &   ⊢ 𝐽 = (invr‘𝑆)    ⇒   ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) = (𝐽‘𝑋))
Theorem	subrgdv 14469	A subring always has the same division function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑆)    &   ⊢ 𝐸 = (/r‘𝑆)    ⇒   ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋𝐸𝑌))
Theorem	subrgunit 14470	An element of a ring is a unit of a subring iff it is a unit of the parent ring and both it and its inverse are in the subring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑉 = (Unit‘𝑆)    &   ⊢ 𝐼 = (invr‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ (𝐼‘𝑋) ∈ 𝐴)))
Theorem	subrgugrp 14471	The units of a subring form a subgroup of the unit group of the original ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑉 = (Unit‘𝑆)    &   ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ∈ (SubGrp‘𝐺))
Theorem	issubrg2 14472*	Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐴 ∈ (SubRing‘𝑅) ↔ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)))
Theorem	subrgnzr 14473	A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ NzRing)
Theorem	subrgintm 14474*	The intersection of an inhabited collection of subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ ∃𝑤 𝑤 ∈ 𝑆) → ∩ 𝑆 ∈ (SubRing‘𝑅))
Theorem	subrgin 14475	The intersection of two subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑅)) → (𝐴 ∩ 𝐵) ∈ (SubRing‘𝑅))
Theorem	subsubrg 14476	A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐵 ∈ (SubRing‘𝑆) ↔ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)))
Theorem	subsubrg2 14477	The set of subrings of a subring are the smaller subrings. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → (SubRing‘𝑆) = ((SubRing‘𝑅) ∩ 𝒫 𝐴))
Theorem	issubrg3 14478	A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ 𝑆 ∈ (SubMnd‘𝑀))))
Theorem	resrhm 14479	Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝑋 ∈ (SubRing‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 RingHom 𝑇))
Theorem	resrhm2b 14480	Restriction of the codomain of a (ring) homomorphism. resghm2b 14063 analog. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubRing‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 RingHom 𝑇) ↔ 𝐹 ∈ (𝑆 RingHom 𝑈)))
Theorem	rhmeql 14481	The equalizer of two ring homomorphisms is a subring. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝐺 ∈ (𝑆 RingHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubRing‘𝑆))
Theorem	rhmima 14482	The homomorphic image of a subring is a subring. (Contributed by Stefan O'Rear, 10-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑋 ∈ (SubRing‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubRing‘𝑁))
Theorem	rnrhmsubrg 14483	The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.)
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → ran 𝐹 ∈ (SubRing‘𝑁))
Theorem	subrgpropd 14484*	If two structures have the same group components (properties), they have the same set of subrings. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (SubRing‘𝐾) = (SubRing‘𝐿))
Theorem	rhmpropd 14485*	Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐽))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝑀))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐽)𝑦) = (𝑥(.r‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝑀)𝑦))    ⇒   ⊢ (𝜑 → (𝐽 RingHom 𝐾) = (𝐿 RingHom 𝑀))
7.3.12  Left regular elements and domains
Syntax	crlreg 14486	Set of left-regular elements in a ring.
class RLReg
Syntax	cdomn 14487	Class of (ring theoretic) domains.
class Domn
Syntax	cidom 14488	Class of integral domains.
class IDomn
Definition	df-rlreg 14489*	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 14490*	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 14491	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ IDomn = (CRing ∩ Domn)
Theorem	rrgmex 14492	A structure whose set of left-regular elements is inhabited is a set. (Contributed by Jim Kingdon, 12-Aug-2025.)
⊢ 𝐸 = (RLReg‘𝑅)    ⇒   ⊢ (𝐴 ∈ 𝐸 → 𝑅 ∈ V)
Theorem	rrgval 14493*	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 14494*	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 14495	Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 ))
Theorem	rrgeq0 14496	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 14497	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)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    &   ⊢ (𝜑 → 𝑌:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 × {𝑋}) ∘𝑓 · 𝑌) supp 0 ) = (𝑌 supp 0 ))
Theorem	rrgss 14498	Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝐸 ⊆ 𝐵
Theorem	unitrrg 14499	Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑈 ⊆ 𝐸)
Theorem	rrgnz 14500	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 ∈ 𝐸)