P. 206 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20501-20600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	issubrg2 20501*	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	opprsubrg 20502	Being a subring is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (SubRing‘𝑅) = (SubRing‘𝑂)
Theorem	subrgnzr 20503	A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ NzRing)
Theorem	subrgint 20504	The intersection of a nonempty 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 20505	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	subrgmre 20506	The subrings of a ring are a Moore system. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (Moore‘𝐵))
Theorem	subsubrg 20507	A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐵 ∈ (SubRing‘𝑆) ↔ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)))
Theorem	subsubrg2 20508	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 20509	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 20510	Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝑋 ∈ (SubRing‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 RingHom 𝑇))
Theorem	resrhm2b 20511	Restriction of the codomain of a (ring) homomorphism. resghm2b 19166 analog. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubRing‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 RingHom 𝑇) ↔ 𝐹 ∈ (𝑆 RingHom 𝑈)))
Theorem	rhmeql 20512	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 20513	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 20514	The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.)
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → ran 𝐹 ∈ (SubRing‘𝑁))
Theorem	cntzsubr 20515	Centralizers in a ring are subrings. (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRing‘𝑅))
Theorem	pwsdiagrhm 20516*	Diagonal homomorphism into a structure power (Rings). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 RingHom 𝑌))
Theorem	subrgpropd 20517*	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 20518*	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 𝑀))
10.3.13.3  Subrings generated by a subset
Syntax	crgspn 20519	Extend class notation with span of a set of elements over a ring.
class RingSpan
Definition	df-rgspn 20520*	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	rgspnval 20521*	Value of the ring-span of a set of elements in a ring. (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴))    ⇒   ⊢ (𝜑 → 𝑈 = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡})
Theorem	rgspncl 20522	The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴))    ⇒   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑅))
Theorem	rgspnssid 20523	The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
Theorem	rgspnmin 20524	The ring-span is contained in all subrings which contain all the generators. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴))    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝑈 ⊆ 𝑆)
10.3.14  Categories of rings
10.3.14.1  The category of non-unital rings The "category of non-unital rings" RngCat is the category of all non-unital rings Rng in a universe and non-unital ring homomorphisms RngHom between these rings. This category is defined as "category restriction" of the category of extensible structures ExtStrCat, which restricts the objects to non-unital rings and the morphisms to the non-unital ring homomorphisms, while the composition of morphisms is preserved, see df-rngc 20526. Alternately, the category of non-unital rings could have been defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, see dfrngc2 20537. Since we consider only "small categories" (i.e. categories whose objects and morphisms are actually sets and not proper classes), the objects of the category (i.e. the base set of the category regarded as extensible structure) are a subset of the non-unital rings (relativized to a subset or "universe" 𝑢) (𝑢 ∩ Rng), see rngcbas 20530, and the morphisms/arrows are the non-unital ring homomorphisms restricted to this subset of the non-unital rings ( RngHom ↾ (𝐵 × 𝐵)), see rngchomfval 20531, whereas the composition is the ordinary composition of functions, see rngccofval 20535 and rngcco 20536. By showing that the non-unital ring homomorphisms between non-unital rings are a subcategory subset (⊆cat) of the mappings between base sets of extensible structures, see rnghmsscmap 20539, it can be shown that the non-unital ring homomorphisms between non-unital rings are a subcategory (Subcat) of the category of extensible structures, see rnghmsubcsetc 20542. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 20543 with the identity function as identity arrow, see rngcid 20544.
Syntax	crngc 20525	Extend class notation to include the category Rng.
class RngCat
Definition	df-rngc 20526	Definition of the category Rng, relativized to a subset 𝑢. This is the category of all non-unital rings in 𝑢 and homomorphisms between these rings. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ RngCat = (𝑢 ∈ V ↦ ((ExtStrCat‘𝑢) ↾cat ( RngHom ↾ ((𝑢 ∩ Rng) × (𝑢 ∩ Rng)))))
Theorem	rngcval 20527	Value of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐶 = ((ExtStrCat‘𝑈) ↾cat 𝐻))
Theorem	rnghmresfn 20528	The class of non-unital ring homomorphisms restricted to subsets of non-unital rings is a function. (Contributed by AV, 4-Mar-2020.)
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝐵 × 𝐵))
Theorem	rnghmresel 20529	An element of the non-unital ring homomorphisms restricted to a subset of non-unital rings is a non-unital ring homomorphisms. (Contributed by AV, 9-Mar-2020.)
⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐹 ∈ (𝑋𝐻𝑌)) → 𝐹 ∈ (𝑋 RngHom 𝑌))
Theorem	rngcbas 20530	Set of objects of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))
Theorem	rngchomfval 20531	Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))
Theorem	rngchom 20532	Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RngHom 𝑌))
Theorem	elrngchom 20533	A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)))
Theorem	rngchomfeqhom 20534	The functionalized Hom-set operation equals the Hom-set operation in the category of non-unital rings (in a universe). (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Homf ‘𝐶) = (Hom ‘𝐶))
Theorem	rngccofval 20535	Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → · = (comp‘(ExtStrCat‘𝑈)))
Theorem	rngcco 20536	Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))    &   ⊢ (𝜑 → 𝐺:(Base‘𝑌)⟶(Base‘𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺 ∘ 𝐹))
Theorem	dfrngc2 20537	Alternate definition of the category of non-unital rings (in a universe). (Contributed by AV, 16-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    &   ⊢ (𝜑 → · = (comp‘(ExtStrCat‘𝑈)))    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Theorem	rnghmsscmap2 20538*	The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory subset of the mappings between base sets of non-unital rings (in the same universe). (Contributed by AV, 6-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (Rng ∩ 𝑈))    ⇒   ⊢ (𝜑 → ( RngHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))))
Theorem	rnghmsscmap 20539*	The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory subset of the mappings between base sets of extensible structures (in the same universe). (Contributed by AV, 9-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (Rng ∩ 𝑈))    ⇒   ⊢ (𝜑 → ( RngHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))))
Theorem	rnghmsubcsetclem1 20540	Lemma 1 for rnghmsubcsetc 20542. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rnghmsubcsetclem2 20541*	Lemma 2 for rnghmsubcsetc 20542. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rnghmsubcsetc 20542	The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory of the category of extensible structures. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶))
Theorem	rngccat 20543	The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 9-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
Theorem	rngcid 20544	The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 10-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑆 = (Base‘𝑋)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = ( I ↾ 𝑆))
Theorem	rngcsect 20545	A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐸 = (Base‘𝑋)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngHom 𝑌) ∧ 𝐺 ∈ (𝑌 RngHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸))))
Theorem	rngcinv 20546	An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑁 = (Inv‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngIso 𝑌) ∧ 𝐺 = ◡𝐹)))
Theorem	rngciso 20547	An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RngIso 𝑌)))
Theorem	rngcifuestrc 20548*	The "inclusion functor" from the category of non-unital rings into the category of extensible structures. (Contributed by AV, 30-Mar-2020.)
⊢ 𝑅 = (RngCat‘𝑈)    &   ⊢ 𝐸 = (ExtStrCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 = ( I ↾ 𝐵))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝐸)𝐺)
Theorem	funcrngcsetc 20549*	The "natural forgetful functor" from the category of non-unital rings into the category of sets which sends each non-unital ring to its underlying set (base set) and the morphisms (non-unital ring homomorphisms) to mappings of the corresponding base sets. An alternate proof is provided in funcrngcsetcALT 20550, using cofuval2 17849 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc 20548, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 18110. (Contributed by AV, 26-Mar-2020.)
⊢ 𝑅 = (RngCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	funcrngcsetcALT 20550*	Alternate proof of funcrngcsetc 20549, using cofuval2 17849 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc 20548, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 18110. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 20549. (Contributed by AV, 30-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑅 = (RngCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	zrinitorngc 20551	The zero ring is an initial object in the category of non-unital rings. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑍 ∈ (InitO‘𝐶))
Theorem	zrtermorngc 20552	The zero ring is a terminal object in the category of non-unital rings. (Contributed by AV, 17-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑍 ∈ (TermO‘𝐶))
Theorem	zrzeroorngc 20553	The zero ring is a zero object in the category of non-unital rings. (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑍 ∈ (ZeroO‘𝐶))
10.3.14.2  The category of (unital) rings The "category of unital rings" RingCat is the category of all (unital) rings Ring in a universe and (unital) ring homomorphisms RingHom between these rings. This category is defined as "category restriction" of the category of extensible structures ExtStrCat, which restricts the objects to (unital) rings and the morphisms to the (unital) ring homomorphisms, while the composition of morphisms is preserved, see df-ringc 20555. Alternately, the category of unital rings could have been defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, see dfringc2 20566. In the following, we omit the predicate "unital", so that "ring" and "ring homomorphism" (without predicate) always mean "unital ring" and "unital ring homomorphism". Since we consider only "small categories" (i.e., categories whose objects and morphisms are actually sets and not proper classes), the objects of the category (i.e. the base set of the category regarded as extensible structure) are a subset of the rings (relativized to a subset or "universe" 𝑢) (𝑢 ∩ Ring), see ringcbas 20559, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom ↾ (𝐵 × 𝐵)), see ringchomfval 20560, whereas the composition is the ordinary composition of functions, see ringccofval 20564 and ringcco 20565. By showing that the ring homomorphisms between rings are a subcategory subset (⊆cat) of the mappings between base sets of extensible structures, see rhmsscmap 20568, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 20571. It follows that the category of rings RingCat is actually a category, see ringccat 20572 with the identity function as identity arrow, see ringcid 20573. Furthermore, it is shown that the ring homomorphisms between rings are a subcategory subset of the non-unital ring homomorphisms between non-unital rings, see rhmsscrnghm 20574, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 20577. By this, the restriction of the category of non-unital rings to the set of unital ring homomorphisms is the category of unital rings, see rngcresringcat 20578: ((RngCat‘𝑈) ↾cat ( RingHom ↾ (𝐵 × 𝐵))) = (RingCat‘𝑈)). Finally, it is shown that the "natural forgetful functor" from the category of rings into the category of sets is the function which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets, see funcringcsetc 20583.
Syntax	cringc 20554	Extend class notation to include the category Ring.
class RingCat
Definition	df-ringc 20555	Definition of the category Ring, relativized to a subset 𝑢. See also the note in [Lang] p. 91, and the item Rng in [Adamek] p. 478. This is the category of all unital rings in 𝑢 and homomorphisms between these rings. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ RingCat = (𝑢 ∈ V ↦ ((ExtStrCat‘𝑢) ↾cat ( RingHom ↾ ((𝑢 ∩ Ring) × (𝑢 ∩ Ring)))))
Theorem	ringcval 20556	Value of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐶 = ((ExtStrCat‘𝑈) ↾cat 𝐻))
Theorem	rhmresfn 20557	The class of unital ring homomorphisms restricted to subsets of unital rings is a function. (Contributed by AV, 10-Mar-2020.)
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝐵 × 𝐵))
Theorem	rhmresel 20558	An element of the unital ring homomorphisms restricted to a subset of unital rings is a unital ring homomorphism. (Contributed by AV, 10-Mar-2020.)
⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐹 ∈ (𝑋𝐻𝑌)) → 𝐹 ∈ (𝑋 RingHom 𝑌))
Theorem	ringcbas 20559	Set of objects of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring))
Theorem	ringchomfval 20560	Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))
Theorem	ringchom 20561	Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌))
Theorem	elringchom 20562	A morphism of unital rings is a function. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)))
Theorem	ringchomfeqhom 20563	The functionalized Hom-set operation equals the Hom-set operation in the category of unital rings (in a universe). (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Homf ‘𝐶) = (Hom ‘𝐶))
Theorem	ringccofval 20564	Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝜑 → · = (comp‘(ExtStrCat‘𝑈)))
Theorem	ringcco 20565	Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))    &   ⊢ (𝜑 → 𝐺:(Base‘𝑌)⟶(Base‘𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺 ∘ 𝐹))
Theorem	dfringc2 20566	Alternate definition of the category of unital rings (in a universe). (Contributed by AV, 16-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    &   ⊢ (𝜑 → · = (comp‘(ExtStrCat‘𝑈)))    ⇒   ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Theorem	rhmsscmap2 20567*	The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the mappings between base sets of unital rings (in the same universe). (Contributed by AV, 6-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    ⇒   ⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))))
Theorem	rhmsscmap 20568*	The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the mappings between base sets of extensible structures (in the same universe). (Contributed by AV, 9-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    ⇒   ⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))))
Theorem	rhmsubcsetclem1 20569	Lemma 1 for rhmsubcsetc 20571. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rhmsubcsetclem2 20570*	Lemma 2 for rhmsubcsetc 20571. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rhmsubcsetc 20571	The unital ring homomorphisms between unital rings (in a universe) are a subcategory of the category of extensible structures. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶))
Theorem	ringccat 20572	The category of unital rings is a category. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 9-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
Theorem	ringcid 20573	The identity arrow in the category of unital rings is the identity function. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 10-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑆 = (Base‘𝑋)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) = ( I ↾ 𝑆))
Theorem	rhmsscrnghm 20574	The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the non-unital ring homomorphisms between non-unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝑆 = (Rng ∩ 𝑈))    ⇒   ⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) ⊆cat ( RngHom ↾ (𝑆 × 𝑆)))
Theorem	rhmsubcrngclem1 20575	Lemma 1 for rhmsubcrngc 20577. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rhmsubcrngclem2 20576*	Lemma 2 for rhmsubcrngc 20577. (Contributed by AV, 12-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rhmsubcrngc 20577	The unital ring homomorphisms between unital rings (in a universe) are a subcategory of the category of non-unital rings. (Contributed by AV, 12-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶))
Theorem	rngcresringcat 20578	The restriction of the category of non-unital rings to the set of unital ring homomorphisms is the category of unital rings. (Contributed by AV, 16-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ (𝜑 → (𝐶 ↾cat 𝐻) = (RingCat‘𝑈))
Theorem	ringcsect 20579	A section in the category of unital rings, written out. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐸 = (Base‘𝑋)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸))))
Theorem	ringcinv 20580	An inverse in the category of unital rings is the converse operation. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑁 = (Inv‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)))
Theorem	ringciso 20581	An isomorphism in the category of unital rings is a bijection. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RingIso 𝑌)))
Theorem	ringcbasbas 20582	An element of the base set of the base set of the category of unital rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    ⇒   ⊢ ((𝜑 ∧ 𝑅 ∈ 𝐵) → (Base‘𝑅) ∈ 𝑈)
Theorem	funcringcsetc 20583*	The "natural forgetful functor" from the category of unital rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 26-Mar-2020.)
⊢ 𝑅 = (RingCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	zrtermoringc 20584	The zero ring is a terminal object in the category of unital rings. (Contributed by AV, 17-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝑍 ∈ (TermO‘𝐶))
Theorem	zrninitoringc 20585*	The zero ring is not an initial object in the category of unital rings (if the universe contains at least one unital ring different from the zero ring). (Contributed by AV, 18-Apr-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → ∃𝑟 ∈ (Base‘𝐶)𝑟 ∈ NzRing)    ⇒   ⊢ (𝜑 → 𝑍 ∉ (InitO‘𝐶))
10.3.14.3  Subcategories of the category of rings
Theorem	srhmsubclem1 20586*	Lemma 1 for srhmsubc 20589. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    ⇒   ⊢ (𝑋 ∈ 𝐶 → 𝑋 ∈ (𝑈 ∩ Ring))
Theorem	srhmsubclem2 20587*	Lemma 2 for srhmsubc 20589. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    ⇒   ⊢ ((𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ (Base‘(RingCat‘𝑈)))
Theorem	srhmsubclem3 20588*	Lemma 3 for srhmsubc 20589. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ ((𝑈 ∈ 𝑉 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐽𝑌) = (𝑋(Hom ‘(RingCat‘𝑈))𝑌))
Theorem	srhmsubc 20589*	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 special ring homomorphisms (i.e., ring homomorphisms from a special ring to another ring of that kind) is a subcategory of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈ (Subcat‘(RingCat‘𝑈)))
Theorem	sringcat 20590*	The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCat‘𝑈) ↾cat 𝐽) ∈ Cat)
Theorem	crhmsubc 20591*	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 commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ CRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈ (Subcat‘(RingCat‘𝑈)))
Theorem	cringcat 20592*	The restriction of the category of (unital) rings to the set of commutative ring homomorphisms is a category, the "category of commutative rings". (Contributed by AV, 19-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ CRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCat‘𝑈) ↾cat 𝐽) ∈ Cat)
Theorem	rngcrescrhm 20593	The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → (𝐶 ↾cat 𝐻) = ((𝐶 ↾s 𝑅) sSet ⟨(Hom ‘ndx), 𝐻⟩))
Theorem	rhmsubclem1 20594	Lemma 1 for rhmsubc 20598. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝑅 × 𝑅))
Theorem	rhmsubclem2 20595	Lemma 2 for rhmsubc 20598. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌))
Theorem	rhmsubclem3 20596*	Lemma 3 for rhmsubc 20598. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((Id‘(RngCat‘𝑈))‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rhmsubclem4 20597*	Lemma 4 for rhmsubc 20598. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(RngCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rhmsubc 20598	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 unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘(RngCat‘𝑈)))
Theorem	rhmsubccat 20599	The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → ((RngCat‘𝑈) ↾cat 𝐻) ∈ Cat)
10.3.15  Left regular elements and domains
Syntax	crlreg 20600	Set of left-regular elements in a ring.
class RLReg