P. 141 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14001-14100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lringnz 14001	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 14002	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)    &   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈))
7.3.11  Subrings
7.3.11.1  Subrings of non-unital rings
Syntax	csubrng 14003	Extend class notation with all subrings of a non-unital ring.
class SubRng
Definition	df-subrng 14004*	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 14005	The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) ↔ (𝑅 ∈ Rng ∧ (𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵))
Theorem	subrngss 14006	A subring is a subset. (Contributed by AV, 14-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝐴 ⊆ 𝐵)
Theorem	subrngid 14007	Every non-unital ring is a subring of itself. (Contributed by AV, 14-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → 𝐵 ∈ (SubRng‘𝑅))
Theorem	subrngrng 14008	A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝑆 ∈ Rng)
Theorem	subrngrcl 14009	Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.)
⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝑅 ∈ Rng)
Theorem	subrngsubg 14010	A subring is a subgroup. (Contributed by AV, 14-Feb-2025.)
⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))
Theorem	subrngringnsg 14011	A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.)
⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝐴 ∈ (NrmSGrp‘𝑅))
Theorem	subrngbas 14012	Base set of a subring structure. (Contributed by AV, 14-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝐴 = (Base‘𝑆))
Theorem	subrng0 14013	A subring always has the same additive identity. (Contributed by AV, 14-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → 0 = (0g‘𝑆))
Theorem	subrngacl 14014	A subring is closed under addition. (Contributed by AV, 14-Feb-2025.)
⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRng‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 + 𝑌) ∈ 𝐴)
Theorem	subrngmcl 14015	A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 14039. (Revised by AV, 14-Feb-2025.)
⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRng‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 · 𝑌) ∈ 𝐴)
Theorem	issubrng2 14016*	Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Rng → (𝐴 ∈ (SubRng‘𝑅) ↔ (𝐴 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)))
Theorem	opprsubrngg 14017	Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (SubRng‘𝑅) = (SubRng‘𝑂))
Theorem	subrngintm 14018*	The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025.)
⊢ ((𝑆 ⊆ (SubRng‘𝑅) ∧ ∃𝑗 𝑗 ∈ 𝑆) → ∩ 𝑆 ∈ (SubRng‘𝑅))
Theorem	subrngin 14019	The intersection of two subrings is a subring. (Contributed by AV, 15-Feb-2025.)
⊢ ((𝐴 ∈ (SubRng‘𝑅) ∧ 𝐵 ∈ (SubRng‘𝑅)) → (𝐴 ∩ 𝐵) ∈ (SubRng‘𝑅))
Theorem	subsubrng 14020	A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → (𝐵 ∈ (SubRng‘𝑆) ↔ (𝐵 ∈ (SubRng‘𝑅) ∧ 𝐵 ⊆ 𝐴)))
Theorem	subsubrng2 14021	The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRng‘𝑅) → (SubRng‘𝑆) = ((SubRng‘𝑅) ∩ 𝒫 𝐴))
Theorem	subrngpropd 14022*	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 14023	Extend class notation with all subrings of a ring.
class SubRing
Syntax	crgspn 14024	Extend class notation with span of a set of elements over a ring.
class RingSpan
Definition	df-subrg 14025*	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 14026*	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 14027	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 14028	A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵)
Theorem	subrgid 14029	Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅))
Theorem	subrgring 14030	A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring)
Theorem	subrgcrng 14031	A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ CRing)
Theorem	subrgrcl 14032	Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
Theorem	subrgsubg 14033	A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.)
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))
Theorem	subrg0 14034	A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 0 = (0g‘𝑆))
Theorem	subrg1cl 14035	A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 ∈ 𝐴)
Theorem	subrgbas 14036	Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆))
Theorem	subrg1 14037	A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 = (1r‘𝑆))
Theorem	subrgacl 14038	A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 + 𝑌) ∈ 𝐴)
Theorem	subrgmcl 14039	A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 · 𝑌) ∈ 𝐴)
Theorem	subrgsubm 14040	A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubMnd‘𝑀))
Theorem	subrgdvds 14041	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 14042	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 14043	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 14044	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 14045	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 14046	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 14047*	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 14048	A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ NzRing)
Theorem	subrgintm 14049*	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 14050	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 14051	A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐵 ∈ (SubRing‘𝑆) ↔ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)))
Theorem	subsubrg2 14052	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 14053	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 14054	Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝑋 ∈ (SubRing‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 RingHom 𝑇))
Theorem	resrhm2b 14055	Restriction of the codomain of a (ring) homomorphism. resghm2b 13642 analog. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubRing‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 RingHom 𝑇) ↔ 𝐹 ∈ (𝑆 RingHom 𝑈)))
Theorem	rhmeql 14056	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 14057	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 14058	The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.)
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → ran 𝐹 ∈ (SubRing‘𝑁))
Theorem	subrgpropd 14059*	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 14060*	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 14061	Set of left-regular elements in a ring.
class RLReg
Syntax	cdomn 14062	Class of (ring theoretic) domains.
class Domn
Syntax	cidom 14063	Class of integral domains.
class IDomn
Definition	df-rlreg 14064*	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 14065*	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 14066	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ IDomn = (CRing ∩ Domn)
Theorem	rrgmex 14067	A structure whose set of left-regular elements is inhabited is a set. (Contributed by Jim Kingdon, 12-Aug-2025.)
⊢ 𝐸 = (RLReg‘𝑅)    ⇒   ⊢ (𝐴 ∈ 𝐸 → 𝑅 ∈ V)
Theorem	rrgval 14068*	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 14069*	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 14070	Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵) → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 ))
Theorem	rrgeq0 14071	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	rrgss 14072	Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝐸 ⊆ 𝐵
Theorem	unitrrg 14073	Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.)
⊢ 𝐸 = (RLReg‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝑈 ⊆ 𝐸)
Theorem	rrgnz 14074	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 14075*	Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
Theorem	domnnzr 14076	A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing)
Theorem	domnring 14077	A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring)
Theorem	domneq0 14078	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 14079	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	opprdomnbg 14080	A class is a domain if and only if its opposite is a domain, biconditional form of opprdomn 14081. (Contributed by SN, 15-Jun-2015.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Domn ↔ 𝑂 ∈ Domn))
Theorem	opprdomn 14081	The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn → 𝑂 ∈ Domn)
Theorem	isidom 14082	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
Theorem	idomdomd 14083	An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Domn)
Theorem	idomcringd 14084	An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) (Proof shortened by SN, 14-May-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
Theorem	idomringd 14085	An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Ring)
7.4  Division rings and fields
7.4.1  Ring apartness
Syntax	capr 14086	Extend class notation with ring apartness.
class #r
Definition	df-apr 14087*	The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 14092. (Contributed by Jim Kingdon, 13-Feb-2025.)
⊢ #r = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤))})
Theorem	aprval 14088	Expand Definition df-apr 14087. (Contributed by Jim Kingdon, 17-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → # = (#r‘𝑅))    &   ⊢ (𝜑 → − = (-g‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (Unit‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 # 𝑌 ↔ (𝑋 − 𝑌) ∈ 𝑈))
Theorem	aprirr 14089	The apartness relation given by df-apr 14087 for a nonzero ring is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → # = (#r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (1r‘𝑅) ≠ (0g‘𝑅))    ⇒   ⊢ (𝜑 → ¬ 𝑋 # 𝑋)
Theorem	aprsym 14090	The apartness relation given by df-apr 14087 for a ring is symmetric. (Contributed by Jim Kingdon, 17-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → # = (#r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 # 𝑌 → 𝑌 # 𝑋))
Theorem	aprcotr 14091	The apartness relation given by df-apr 14087 for a local ring is cotransitive. (Contributed by Jim Kingdon, 17-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → # = (#r‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ LRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 # 𝑌 → (𝑋 # 𝑍 ∨ 𝑌 # 𝑍)))
Theorem	aprap 14092	The relation given by df-apr 14087 for a local ring is an apartness relation. (Contributed by Jim Kingdon, 20-Feb-2025.)
⊢ (𝑅 ∈ LRing → (#r‘𝑅) Ap (Base‘𝑅))
7.5  Left modules
7.5.1  Definition and basic properties
Syntax	clmod 14093	Extend class notation with class of all left modules.
class LMod
Syntax	cscaf 14094	The functionalization of the scalar multiplication operation.
class ·sf
Definition	df-lmod 14095*	Define the class of all left modules, which are generalizations of left vector spaces. A left module over a ring is an (Abelian) group (vectors) together with a ring (scalars) and a left scalar product connecting them. (Contributed by NM, 4-Nov-2013.)
⊢ LMod = {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))}
Definition	df-scaf 14096*	Define the functionalization of the ·𝑠 operator. This restricts the value of ·𝑠 to the stated domain, which is necessary when working with restricted structures, whose operations may be defined on a larger set than the true base. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ ·sf = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦)))
Theorem	islmod 14097*	The predicate "is a left module". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ⨣ = (+g‘𝐹)    &   ⊢ × = (.r‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    ⇒   ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
Theorem	lmodlema 14098	Lemma for properties of a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ⨣ = (+g‘𝐹)    &   ⊢ × = (.r‘𝐹)    &   ⊢ 1 = (1r‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌)))
Theorem	islmodd 14099*	Properties that determine a left module. See note in isgrpd2 13397 regarding the 𝜑 on hypotheses that name structure components. (Contributed by Mario Carneiro, 22-Jun-2014.)
⊢ (𝜑 → 𝑉 = (Base‘𝑊))    &   ⊢ (𝜑 → + = (+g‘𝑊))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))    &   ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐹))    &   ⊢ (𝜑 → ⨣ = (+g‘𝐹))    &   ⊢ (𝜑 → × = (.r‘𝐹))    &   ⊢ (𝜑 → 1 = (1r‘𝐹))    &   ⊢ (𝜑 → 𝐹 ∈ Ring)    &   ⊢ (𝜑 → 𝑊 ∈ Grp)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉) → (𝑥 · 𝑦) ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 1 · 𝑥) = 𝑥)    ⇒   ⊢ (𝜑 → 𝑊 ∈ LMod)
Theorem	lmodgrp 14100	A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.)
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)