P. 207 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	subrgsubm 20601	A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubMnd‘𝑀))
Theorem	subrgdvds 20602	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 20603	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 20604	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 20605	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 20606	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 20607	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 20608*	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 20609	Being a subring is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (SubRing‘𝑅) = (SubRing‘𝑂)
Theorem	subrgnzr 20610	A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ NzRing)
Theorem	subrgint 20611	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 20612	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 20613	The subrings of a ring are a Moore system. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (Moore‘𝐵))
Theorem	subsubrg 20614	A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐵 ∈ (SubRing‘𝑆) ↔ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)))
Theorem	subsubrg2 20615	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 20616	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 20617	Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝑋 ∈ (SubRing‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 RingHom 𝑇))
Theorem	resrhm2b 20618	Restriction of the codomain of a (ring) homomorphism. resghm2b 19264 analog. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubRing‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 RingHom 𝑇) ↔ 𝐹 ∈ (𝑆 RingHom 𝑈)))
Theorem	rhmeql 20619	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 20620	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 20621	The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.)
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → ran 𝐹 ∈ (SubRing‘𝑁))
Theorem	cntzsubr 20622	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 20623*	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 20624*	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 20625*	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 20626	Extend class notation with span of a set of elements over a ring.
class RingSpan
Definition	df-rgspn 20627*	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 20628*	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 20629	The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴))    ⇒   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑅))
Theorem	rgspnssid 20630	The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅))    &   ⊢ (𝜑 → 𝑈 = (𝑁‘𝐴))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
Theorem	rgspnmin 20631	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 20633. 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 20644. 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 20637, and the morphisms/arrows are the non-unital ring homomorphisms restricted to this subset of the non-unital rings ( RngHom ↾ (𝐵 × 𝐵)), see rngchomfval 20638, whereas the composition is the ordinary composition of functions, see rngccofval 20642 and rngcco 20643. 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 20646, 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 20649. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 20650 with the identity function as identity arrow, see rngcid 20651.
Syntax	crngc 20632	Extend class notation to include the category Rng.
class RngCat
Definition	df-rngc 20633	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 20634	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 20635	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 20636	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 20637	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 20638	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 20639	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 20640	A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)))
Theorem	rngchomfeqhom 20641	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 20642	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 20643	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 20644	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 20645*	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 20646*	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 20647	Lemma 1 for rnghmsubcsetc 20649. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rnghmsubcsetclem2 20648*	Lemma 2 for rnghmsubcsetc 20649. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RngHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rnghmsubcsetc 20649	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 20650	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 20651	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 20652	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 20653	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 20654	An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RngIso 𝑌)))
Theorem	rngcifuestrc 20655*	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 20656*	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 20657, using cofuval2 17937 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 20655, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 18204. (Contributed by AV, 26-Mar-2020.)
⊢ 𝑅 = (RngCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	funcrngcsetcALT 20657*	Alternate proof of funcrngcsetc 20656, using cofuval2 17937 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 20655, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 18204. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 20656. (Contributed by AV, 30-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑅 = (RngCat‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	zrinitorngc 20658	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 20659	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 20660	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 20662. 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 20673. 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 20666, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom ↾ (𝐵 × 𝐵)), see ringchomfval 20667, whereas the composition is the ordinary composition of functions, see ringccofval 20671 and ringcco 20672. By showing that the ring homomorphisms between rings are a subcategory subset (⊆cat) of the mappings between base sets of extensible structures, see rhmsscmap 20675, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 20678. It follows that the category of rings RingCat is actually a category, see ringccat 20679 with the identity function as identity arrow, see ringcid 20680. 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 20681, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 20684. 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 20685: ((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 20690.
Syntax	cringc 20661	Extend class notation to include the category Ring.
class RingCat
Definition	df-ringc 20662	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 20663	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 20664	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 20665	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 20666	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 20667	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 20668	Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌))
Theorem	elringchom 20669	A morphism of unital rings is a function. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)))
Theorem	ringchomfeqhom 20670	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 20671	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 20672	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 20673	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 20674*	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 20675*	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 20676	Lemma 1 for rhmsubcsetc 20678. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rhmsubcsetclem2 20677*	Lemma 2 for rhmsubcsetc 20678. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (ExtStrCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rhmsubcsetc 20678	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 20679	The category of unital rings is a category. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 9-Mar-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
Theorem	ringcid 20680	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 20681	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 20682	Lemma 1 for rhmsubcrngc 20684. (Contributed by AV, 9-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rhmsubcrngclem2 20683*	Lemma 2 for rhmsubcrngc 20684. (Contributed by AV, 12-Mar-2020.)
⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Ring ∩ 𝑈))    &   ⊢ (𝜑 → 𝐻 = ( RingHom ↾ (𝐵 × 𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rhmsubcrngc 20684	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 20685	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 20686	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 20687	An inverse in the category of unital rings is the converse operation. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑁 = (Inv‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)))
Theorem	ringciso 20688	An isomorphism in the category of unital rings is a bijection. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐶 = (RingCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RingIso 𝑌)))
Theorem	ringcbasbas 20689	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 20690*	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 20691	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 20692*	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 20693*	Lemma 1 for srhmsubc 20696. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    ⇒   ⊢ (𝑋 ∈ 𝐶 → 𝑋 ∈ (𝑈 ∩ Ring))
Theorem	srhmsubclem2 20694*	Lemma 2 for srhmsubc 20696. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    ⇒   ⊢ ((𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ (Base‘(RingCat‘𝑈)))
Theorem	srhmsubclem3 20695*	Lemma 3 for srhmsubc 20696. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ ((𝑈 ∈ 𝑉 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐽𝑌) = (𝑋(Hom ‘(RingCat‘𝑈))𝑌))
Theorem	srhmsubc 20696*	According to df-subc 17859, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17890 and subcss2 17893). 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 20697*	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 20698*	According to df-subc 17859, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17890 and subcss2 17893). 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 20699*	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 20700	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), 𝐻⟩))