P. 421 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42001-42100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zrtermorngc 42001	The zero ring is a terminal object in the category of nonunital rings. (Contributed by AV, 17-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   =>    |- ( ph -> Z e. (TermO ` C ) )
Theorem	zrzeroorngc 42002	The zero ring is a zero object in the category of non-unital rings. (Contributed by AV, 18-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   =>    |- ( ph -> Z e. (ZeroO ` C ) )
20.35.14.9  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 42005. 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 42018. 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" u) ( u i^i Ring ), see ringcbas 42011, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom |` ( B X. B ) ), see ringchomfval 42012, whereas the composition is the ordinary composition of functions, see ringccofval 42016 and ringcco 42017. By showing that the ring homomorphisms between rings are a subcategory subset ( C_cat) of the mappings between base sets of extensible structures, see rhmsscmap 42020, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 42023. It follows that the category of rings RingCat is actually a category, see ringccat 42024 with the identity function as identity arrow, see ringcid 42025. 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 42026, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 42029. 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 42030: ( (RngCat ` U ) |`cat ( RingHom |` ( B X. B ) ) ) = (RingCat ` U ) ). 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 42035.
Syntax	cringc 42003	Extend class notation to include the category Ring.
class RingCat
Syntax	cringcALTV 42004	Extend class notation to include the category Ring. (New usage is discouraged.)
class RingCatALTV
Definition	df-ringc 42005	Definition of the category Ring, relativized to a subset u. 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 u and homomorphisms between these rings. Generally, we will take u 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 = ( u e. _V |-> ( (ExtStrCat ` u ) |`cat ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) ) )
Definition	df-ringcALTV 42006*	Definition of the category Ring, relativized to a subset u. This is the category of all rings in u and homomorphisms between these rings. Generally, we will take u 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.) (New usage is discouraged.)
|- RingCatALTV = ( u e. _V |-> [_ ( u i^i Ring ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RingHom y ) ) >. , <. (comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RingHom z ) , f e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } )
Theorem	ringcvalALTV 42007*	Value of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Ring ) )   &    |- ( ph -> H = ( x e. B , y e. B |-> ( x RingHom y ) ) )   &    |- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RingHom z ) , f e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	ringcval 42008	Value of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RingCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Ring ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ph -> C = ( (ExtStrCat ` U ) |`cat H ) )
Theorem	rhmresfn 42009	The class of unital ring homomorphisms restricted to subsets of unital rings is a function. (Contributed by AV, 10-Mar-2020.)
|- ( ph -> B = ( U i^i Ring ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ph -> H Fn ( B X. B ) )
Theorem	rhmresel 42010	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.)
|- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) /\ F e. ( X H Y ) ) -> F e. ( X RingHom Y ) )
Theorem	ringcbas 42011	Set of objects of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> B = ( U i^i Ring ) )
Theorem	ringchomfval 42012	Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )
Theorem	ringchom 42013	Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X H Y ) = ( X RingHom Y ) )
Theorem	elringchom 42014	A morphism of unital rings is a function. (Contributed by AV, 14-Feb-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( F e. ( X H Y ) -> F : ( Base ` X ) --> ( Base ` Y ) ) )
Theorem	ringchomfeqhom 42015	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.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> ( Hom f ` C ) = ( Hom ` C ) )
Theorem	ringccofval 42016	Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RingCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   =>    |- ( ph -> .x. = (comp ` (ExtStrCat ` U ) ) )
Theorem	ringcco 42017	Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RingCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- ( ph -> Z e. U )   &    |- ( ph -> F : ( Base ` X ) --> ( Base ` Y ) )   &    |- ( ph -> G : ( Base ` Y ) --> ( Base ` Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )
Theorem	dfringc2 42018	Alternate definition of the category of unital rings (in a universe). (Contributed by AV, 16-Mar-2020.)
|- C = (RingCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Ring ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   &    |- ( ph -> .x. = (comp ` (ExtStrCat ` U ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	rhmsscmap2 42019*	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.)
|- ( ph -> U e. V )   &    |- ( ph -> R = ( Ring i^i U ) )   =>    |- ( ph -> ( RingHom |` ( R X. R ) ) C_cat ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
Theorem	rhmsscmap 42020*	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.)
|- ( ph -> U e. V )   &    |- ( ph -> R = ( Ring i^i U ) )   =>    |- ( ph -> ( RingHom |` ( R X. R ) ) C_cat ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
Theorem	rhmsubcsetclem1 42021	Lemma 1 for rhmsubcsetc 42023. (Contributed by AV, 9-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )
Theorem	rhmsubcsetclem2 42022*	Lemma 2 for rhmsubcsetc 42023. (Contributed by AV, 9-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ( ph /\ x e. B ) -> A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. (comp ` C ) z ) f ) e. ( x H z ) )
Theorem	rhmsubcsetc 42023	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.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ph -> H e. (Subcat ` C ) )
Theorem	ringccat 42024	The category of unital rings is a category. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 9-Mar-2020.)
|- C = (RingCat ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	ringcid 42025	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.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- S = ( Base ` X )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` S ) )
Theorem	rhmsscrnghm 42026	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.)
|- ( ph -> U e. V )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- ( ph -> S = (Rng i^i U ) )   =>    |- ( ph -> ( RingHom |` ( R X. R ) ) C_cat ( RngHomo |` ( S X. S ) ) )
Theorem	rhmsubcrngclem1 42027	Lemma 1 for rhmsubcrngc 42029. (Contributed by AV, 9-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )
Theorem	rhmsubcrngclem2 42028*	Lemma 2 for rhmsubcrngc 42029. (Contributed by AV, 12-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ( ph /\ x e. B ) -> A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. (comp ` C ) z ) f ) e. ( x H z ) )
Theorem	rhmsubcrngc 42029	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.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ph -> H e. (Subcat ` C ) )
Theorem	rngcresringcat 42030	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.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ph -> ( C |`cat H ) = (RingCat ` U ) )
Theorem	ringcsect 42031	A section in the category of unital rings, written out. (Contributed by AV, 14-Feb-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- E = ( Base ` X )   &    |- S = (Sect ` C )   =>    |- ( ph -> ( F ( X S Y ) G <-> ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) /\ ( G o. F ) = ( _I |` E ) ) ) )
Theorem	ringcinv 42032	An inverse in the category of unital rings is the converse operation. (Contributed by AV, 14-Feb-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- N = (Inv ` C )   =>    |- ( ph -> ( F ( X N Y ) G <-> ( F e. ( X RingIso Y ) /\ G = `' F ) ) )
Theorem	ringciso 42033	An isomorphism in the category of unital rings is a bijection. (Contributed by AV, 14-Feb-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   =>    |- ( ph -> ( F e. ( X I Y ) <-> F e. ( X RingIso Y ) ) )
Theorem	ringcbasbas 42034	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.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. WUni )   =>    |- ( ( ph /\ R e. B ) -> ( Base ` R ) e. U )
Theorem	funcringcsetc 42035*	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.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ph -> F ( R Func S ) G )
Theorem	funcringcsetcALTV2lem1 42036*	Lemma 1 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( F ` X ) = ( Base ` X ) )
Theorem	funcringcsetcALTV2lem2 42037*	Lemma 2 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( F ` X ) e. U )
Theorem	funcringcsetcALTV2lem3 42038*	Lemma 3 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ph -> F : B --> C )
Theorem	funcringcsetcALTV2lem4 42039*	Lemma 4 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ph -> G Fn ( B X. B ) )
Theorem	funcringcsetcALTV2lem5 42040*	Lemma 5 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X G Y ) = ( _I |` ( X RingHom Y ) ) )
Theorem	funcringcsetcALTV2lem6 42041*	Lemma 6 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( X RingHom Y ) ) -> ( ( X G Y ) ` H ) = H )
Theorem	funcringcsetcALTV2lem7 42042*	Lemma 7 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( ( X G X ) ` ( ( Id ` R ) ` X ) ) = ( ( Id ` S ) ` ( F ` X ) ) )
Theorem	funcringcsetcALTV2lem8 42043*	Lemma 8 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X G Y ) : ( X ( Hom ` R ) Y ) --> ( ( F ` X ) ( Hom ` S ) ( F ` Y ) ) )
Theorem	funcringcsetcALTV2lem9 42044*	Lemma 9 for funcringcsetcALTV2 42045. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( H e. ( X ( Hom ` R ) Y ) /\ K e. ( Y ( Hom ` R ) Z ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. (comp ` R ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. (comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) )
Theorem	funcringcsetcALTV2 42045*	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, 16-Feb-2020.) (New usage is discouraged.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ph -> F ( R Func S ) G )
Theorem	ringcbasALTV 42046	Set of objects of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> B = ( U i^i Ring ) )
Theorem	ringchomfvalALTV 42047*	Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( x e. B , y e. B |-> ( x RingHom y ) ) )
Theorem	ringchomALTV 42048	Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X H Y ) = ( X RingHom Y ) )
Theorem	elringchomALTV 42049	A morphism of rings is a function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( F e. ( X H Y ) -> F : ( Base ` X ) --> ( Base ` Y ) ) )
Theorem	ringccofvalALTV 42050*	Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   =>    |- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RingHom z ) , f e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) )
Theorem	ringccoALTV 42051	Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X RingHom Y ) )   &    |- ( ph -> G e. ( Y RingHom Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )
Theorem	ringccatidALTV 42052*	Lemma for ringccatALTV 42053. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   =>    |- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( _I |` ( Base ` x ) ) ) ) )
Theorem	ringccatALTV 42053	The category of rings is a category. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	ringcidALTV 42054	The identity arrow in the category of rings is the identity function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- S = ( Base ` X )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` S ) )
Theorem	ringcsectALTV 42055	A section in the category of rings, written out. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- E = ( Base ` X )   &    |- S = (Sect ` C )   =>    |- ( ph -> ( F ( X S Y ) G <-> ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) /\ ( G o. F ) = ( _I |` E ) ) ) )
Theorem	ringcinvALTV 42056	An inverse in the category of rings is the converse operation. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- N = (Inv ` C )   =>    |- ( ph -> ( F ( X N Y ) G <-> ( F e. ( X RingIso Y ) /\ G = `' F ) ) )
Theorem	ringcisoALTV 42057	An isomorphism in the category of rings is a bijection. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   =>    |- ( ph -> ( F e. ( X I Y ) <-> F e. ( X RingIso Y ) ) )
Theorem	ringcbasbasALTV 42058	An element of the base set of the base set of the category of rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. WUni )   =>    |- ( ( ph /\ R e. B ) -> ( Base ` R ) e. U )
Theorem	funcringcsetclem1ALTV 42059*	Lemma 1 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( F ` X ) = ( Base ` X ) )
Theorem	funcringcsetclem2ALTV 42060*	Lemma 2 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( F ` X ) e. U )
Theorem	funcringcsetclem3ALTV 42061*	Lemma 3 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ph -> F : B --> C )
Theorem	funcringcsetclem4ALTV 42062*	Lemma 4 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ph -> G Fn ( B X. B ) )
Theorem	funcringcsetclem5ALTV 42063*	Lemma 5 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X G Y ) = ( _I |` ( X RingHom Y ) ) )
Theorem	funcringcsetclem6ALTV 42064*	Lemma 6 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( X RingHom Y ) ) -> ( ( X G Y ) ` H ) = H )
Theorem	funcringcsetclem7ALTV 42065*	Lemma 7 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( ( X G X ) ` ( ( Id ` R ) ` X ) ) = ( ( Id ` S ) ` ( F ` X ) ) )
Theorem	funcringcsetclem8ALTV 42066*	Lemma 8 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X G Y ) : ( X ( Hom ` R ) Y ) --> ( ( F ` X ) ( Hom ` S ) ( F ` Y ) ) )
Theorem	funcringcsetclem9ALTV 42067*	Lemma 9 for funcringcsetcALTV 42068. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( H e. ( X ( Hom ` R ) Y ) /\ K e. ( Y ( Hom ` R ) Z ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. (comp ` R ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. (comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) )
Theorem	funcringcsetcALTV 42068*	The "natural forgetful functor" from the category of 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, 16-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ph -> F ( R Func S ) G )
Theorem	irinitoringc 42069	The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of [Adamek] p. 101 , and example in [Lang] p. 58. (Contributed by AV, 3-Apr-2020.)
|- ( ph -> U e. V )   &    |- ( ph -> ℤring e. U )   &    |- C = (RingCat ` U )   =>    |- ( ph -> ℤring e. (InitO ` C ) )
Theorem	zrtermoringc 42070	The zero ring is a terminal object in the category of unital rings. (Contributed by AV, 17-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RingCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   =>    |- ( ph -> Z e. (TermO ` C ) )
Theorem	zrninitoringc 42071*	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.)
|- ( ph -> U e. V )   &    |- C = (RingCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   &    |- ( ph -> E. r e. ( Base ` C ) r e. NzRing )   =>    |- ( ph -> Z e/ (InitO ` C ) )
Theorem	nzerooringczr 42072	There is no zero object in the category of unital rings (at least in a universe which contains the zero ring and the ring of integers). Example 7.9 (3) in [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RingCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   &    |- ( ph -> ℤring e. U )   =>    |- ( ph -> (ZeroO ` C ) = (/) )
20.35.14.10  Subcategories of the category of rings
Theorem	srhmsubclem1 42073*	Lemma 1 for srhmsubc 42076. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   =>    |- ( X e. C -> X e. ( U i^i Ring ) )
Theorem	srhmsubclem2 42074*	Lemma 2 for srhmsubc 42076. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   =>    |- ( ( U e. V /\ X e. C ) -> X e. ( Base ` (RingCat ` U ) ) )
Theorem	srhmsubclem3 42075*	Lemma 3 for srhmsubc 42076. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> ( X J Y ) = ( X ( Hom ` (RingCat ` U ) ) Y ) )
Theorem	srhmsubc 42076*	According to df-subc 16472, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 16500 and subcss2 16503). 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.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCat ` U ) ) )
Theorem	sringcat 42077*	The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCat ` U ) |`cat J ) e. Cat )
Theorem	crhmsubc 42078*	According to df-subc 16472, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 16500 and subcss2 16503). 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.)
|- C = ( U i^i CRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCat ` U ) ) )
Theorem	cringcat 42079*	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.)
|- C = ( U i^i CRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCat ` U ) |`cat J ) e. Cat )
Theorem	drhmsubc 42080*	According to df-subc 16472, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 16500 and subcss2 16503). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCat ` U ) ) )
Theorem	drngcat 42081*	The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCat ` U ) |`cat J ) e. Cat )
Theorem	fldcat 42082*	The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCat ` U ) |`cat F ) e. Cat )
Theorem	fldc 42083*	The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( ( (RingCat ` U ) |`cat J ) |`cat F ) e. Cat )
Theorem	fldhmsubc 42084*	According to df-subc 16472, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 16500 and subcss2 16503). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> F e. (Subcat ` ( (RingCat ` U ) |`cat J ) ) )
Theorem	rngcrescrhm 42085	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.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> ( C |`cat H ) = ( ( C ↾s R ) sSet <. ( Hom ` ndx ) , H >. ) )
Theorem	rhmsubclem1 42086	Lemma 1 for rhmsubc 42090. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> H Fn ( R X. R ) )
Theorem	rhmsubclem2 42087	Lemma 2 for rhmsubc 42090. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ph /\ X e. R /\ Y e. R ) -> ( X H Y ) = ( X RingHom Y ) )
Theorem	rhmsubclem3 42088*	Lemma 3 for rhmsubc 42090. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ph /\ x e. R ) -> ( ( Id ` (RngCat ` U ) ) ` x ) e. ( x H x ) )
Theorem	rhmsubclem4 42089*	Lemma 4 for rhmsubc 42090. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. (comp ` (RngCat ` U ) ) z ) f ) e. ( x H z ) )
Theorem	rhmsubc 42090	According to df-subc 16472, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 16500 and subcss2 16503). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> H e. (Subcat ` (RngCat ` U ) ) )
Theorem	rhmsubccat 42091	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.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> ( (RngCat ` U ) |`cat H ) e. Cat )
Theorem	srhmsubcALTVlem1 42092*	Lemma 1 for srhmsubcALTV 42094. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   =>    |- ( ( U e. V /\ X e. C ) -> X e. ( Base ` (RingCatALTV ` U ) ) )
Theorem	srhmsubcALTVlem2 42093*	Lemma 2 for srhmsubcALTV 42094. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> ( X J Y ) = ( X ( Hom ` (RingCatALTV ` U ) ) Y ) )
Theorem	srhmsubcALTV 42094*	According to df-subc 16472, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 16500 and subcss2 16503). 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.) (New usage is discouraged.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCatALTV ` U ) ) )
Theorem	sringcatALTV 42095*	The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCatALTV ` U ) |`cat J ) e. Cat )
Theorem	crhmsubcALTV 42096*	According to df-subc 16472, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 16500 and subcss2 16503). 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.) (New usage is discouraged.)
|- C = ( U i^i CRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCatALTV ` U ) ) )
Theorem	cringcatALTV 42097*	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.) (New usage is discouraged.)
|- C = ( U i^i CRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCatALTV ` U ) |`cat J ) e. Cat )
Theorem	drhmsubcALTV 42098*	According to df-subc 16472, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 16500 and subcss2 16503). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCatALTV ` U ) ) )
Theorem	drngcatALTV 42099*	The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCatALTV ` U ) |`cat J ) e. Cat )
Theorem	fldcatALTV 42100*	The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCatALTV ` U ) |`cat F ) e. Cat )