P. 331 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33001-33100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lidlssbas 33001	The base set of the restriction of the ring to a (left) ideal is a subset of the base set of the ring. (Contributed by AV, 17-Feb-2020.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   =>    |- ( U e. L -> ( Base ` I ) C_ ( Base ` R ) )
Theorem	lidlbas 33002	A (left) ideal of a ring is the base set of the restriction of the ring to this ideal. (Contributed by AV, 17-Feb-2020.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   =>    |- ( U e. L -> ( Base ` I ) = U )
Theorem	lidlabl 33003	A (left) ideal of a ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   =>    |- ( ( R e. Ring /\ U e. L ) -> I e. Abel )
Theorem	lidlmmgm 33004	The multiplicative group of a (left) ideal of a ring is a magma. (Contributed by AV, 17-Feb-2020.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   =>    |- ( ( R e. Ring /\ U e. L ) -> (mulGrp ` I ) e. Mgm )
Theorem	lidlmsgrp 33005	The multiplicative group of a (left) ideal of a ring is a semigroup. (Contributed by AV, 17-Feb-2020.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   =>    |- ( ( R e. Ring /\ U e. L ) -> (mulGrp ` I ) e. SGrp )
Theorem	lidlrng 33006	A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   =>    |- ( ( R e. Ring /\ U e. L ) -> I e. Rng )
Theorem	zlidlring 33007	The zero (left) ideal of a non-unital ring is a unital ring (the zero ring). (Contributed by AV, 16-Feb-2020.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ U = { .0. } ) -> I e. Ring )
Theorem	uzlidlring 33008	Only the zero (left) ideal or the unit (left) ideal of a domain is a unital ring. (Contributed by AV, 18-Feb-2020.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Domn /\ U e. L ) -> ( I e. Ring <-> ( U = { .0. } \/ U = B ) ) )
Theorem	lidldomnnring 33009	A (left) ideal of a domain which is neither the zero ideal nor the unit ideal is not a unital ring. (Contributed by AV, 18-Feb-2020.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } /\ U =/= B ) ) -> I e/ Ring )
21.24.10.6  The non-unital ring of even integers
Theorem	0even 33010*	0 is an even integer. (Contributed by AV, 11-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   =>    |- 0 e. E
Theorem	1neven 33011*	1 is not an even integer. (Contributed by AV, 12-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   =>    |- 1 e/ E
Theorem	2even 33012*	2 is an even integer. (Contributed by AV, 12-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   =>    |- 2 e. E
Theorem	2zlidl 33013*	The even integers are a (left) ideal of the ring of integers. (Contributed by AV, 20-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- U = (LIdeal ` ℤring )   =>    |- E e. U
Theorem	2zrng 33014*	The ring of integers restricted to the even integers is a (non-unital) ring, the "ring of even integers". Remark: the structure of the complementary subset of the set of integers, the odd integers, is not even a magma, see oddinmgm 32894. (Contributed by AV, 20-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- U = (LIdeal ` ℤring )   &    |- R = (ℤring ↾s E )   =>    |- R e. Rng
Theorem	2zrngbas 33015*	The base set of R is the set of all even integers. (Contributed by AV, 31-Jan-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   =>    |- E = ( Base ` R )
Theorem	2zrngadd 33016*	The group addition operation of R is the addition of complex numbers. (Contributed by AV, 31-Jan-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   =>    |- + = ( +g ` R )
Theorem	2zrng0 33017*	The additive identity of R is the complex number 0. (Contributed by AV, 11-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   =>    |- 0 = ( 0g ` R )
Theorem	2zrngamgm 33018*	R is an (additive) magma. (Contributed by AV, 6-Jan-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   =>    |- R e. Mgm
Theorem	2zrngasgrp 33019*	R is an (additive) semigroup. (Contributed by AV, 4-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   =>    |- R e. SGrp
Theorem	2zrngamnd 33020*	R is an (additive) monoid. (Contributed by AV, 11-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   =>    |- R e. Mnd
Theorem	2zrngacmnd 33021*	R is a commutative (additive) monoid. (Contributed by AV, 11-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   =>    |- R e. CMnd
Theorem	2zrngagrp 33022*	R is an (additive) group. (Contributed by AV, 6-Jan-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   =>    |- R e. Grp
Theorem	2zrngaabl 33023*	R is an (additive) abelian group. (Contributed by AV, 11-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   =>    |- R e. Abel
Theorem	2zrngmul 33024*	The ring multiplication operation of R is the multiplication on complex numbers. (Contributed by AV, 31-Jan-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   =>    |- x. = ( .r ` R )
Theorem	2zrngmmgm 33025*	R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   &    |- M = (mulGrp ` R )   =>    |- M e. Mgm
Theorem	2zrngmsgrp 33026*	R is a (multiplicative) semigroup. (Contributed by AV, 4-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   &    |- M = (mulGrp ` R )   =>    |- M e. SGrp
Theorem	2zrngALT 33027*	The ring of integers restricted to the even integers is a (non-unital) ring, the "ring of even integers". Alternate version of 2zrng 33014, based on a restriction of the field of the complex numbers. The proof is based on the facts that the ring of even integers is an additive abelian group (see 2zrngaabl 33023) and a multiplicative semigroup (see 2zrngmsgrp 33026). (Contributed by AV, 11-Feb-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   &    |- M = (mulGrp ` R )   =>    |- R e. Rng
Theorem	2zrngnmlid 33028*	R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   &    |- M = (mulGrp ` R )   =>    |- A. b e. E E. a e. E ( b x. a ) =/= a
Theorem	2zrngnmrid 33029*	R has no multiplicative (right) identity. (Contributed by AV, 12-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   &    |- M = (mulGrp ` R )   =>    |- A. a e. ( E \ { 0 } ) A. b e. E ( a x. b ) =/= a
Theorem	2zrngnmlid2 33030*	R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   &    |- M = (mulGrp ` R )   =>    |- A. a e. ( E \ { 0 } ) A. b e. E ( b x. a ) =/= a
Theorem	2zrngnring 33031*	R is not a unital ring. (Contributed by AV, 6-Jan-2020.)
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }   &    |- R = (ℂfld ↾s E )   &    |- M = (mulGrp ` R )   =>    |- R e/ Ring
21.24.10.7  A constructed not unital ring
Theorem	plusgndxnmulrndx 33032	The slot for the group (addition) operation is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 16-Feb-2020.)
|- ( +g ` ndx ) =/= ( .r ` ndx )
Theorem	basendxnmulrndx 33033	The slot for the base set is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 16-Feb-2020.)
|- ( Base ` ndx ) =/= ( .r ` ndx )
Theorem	cznrnglem 33034	Lemma for cznrng 33036: The base set of the ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is the base set of the ℤ/nℤ structure. (Contributed by AV, 16-Feb-2020.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   &    |- X = ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. )   =>    |- B = ( Base ` X )
Theorem	cznabel 33035	The ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is an abelian group. (Contributed by AV, 16-Feb-2020.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   &    |- X = ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. )   =>    |- ( ( N e. NN /\ C e. B ) -> X e. Abel )
Theorem	cznrng 33036*	The ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is a non-unital ring. (Contributed by AV, 17-Feb-2020.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   &    |- X = ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. )   &    |- .0. = ( 0g ` Y )   =>    |- ( ( N e. NN /\ C = .0. ) -> X e. Rng )
Theorem	cznnring 33037*	The ring constructed from a ℤ/nℤ structure with 1 < n by replacing the (multiplicative) ring operation by a constant operation is not a unital ring. (Contributed by AV, 17-Feb-2020.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   &    |- X = ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. )   &    |- .0. = ( 0g ` Y )   =>    |- ( ( N e. ( ZZ>= ` 2 ) /\ C e. B ) -> X e/ Ring )
21.24.10.8  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 RngHomo 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 33040. Alternatively, 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 df-rngcALTV 33041 or dfrngc2 33053. 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" u) ( u i^i Rng ), see rngcbas 33046, and the morphisms/arrows are the non-unital ring homomorphisms restricted to this subset of the non-unital rings ( RngHomo |` ( B X. B ) ), see rngchomfval 33047, whereas the composition is the ordinary composition of functions, see rngccofval 33051 and rngcco 33052. By showing that the non-unital ring homomorphisms between non-unital rings are a subcategory subset ( C_cat) of the mappings between base sets of extensible structures, see rnghmsscmap 33055, 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 33058. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 33059 with the identity function as identity arrow, see rngcid 33060.
Syntax	crngc 33038	Extend class notation to include the category Rng.
class RngCat
Syntax	crngcALTV 33039	Extend class notation to include the category Rng. (New usage is discouraged.)
class RngCatALTV
Definition	df-rngc 33040	Definition of the category Rng, relativized to a subset u. This is the category of all non-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, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- RngCat = ( u e. _V |-> ( (ExtStrCat ` u ) |`cat ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) ) )
Definition	df-rngcALTV 33041*	Definition of the category Rng, relativized to a subset u. This is the category of all non-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. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- RngCatALTV = ( u e. _V |-> [_ ( u i^i Rng ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHomo y ) ) >. , <. (comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } )
Theorem	rngcvalALTV 33042*	Value of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Rng ) )   &    |- ( ph -> H = ( x e. B , y e. B |-> ( x RngHomo y ) ) )   &    |- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	rngcval 33043	Value of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Rng ) )   &    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   =>    |- ( ph -> C = ( (ExtStrCat ` U ) |`cat H ) )
Theorem	rnghmresfn 33044	The class of non-unital ring homomorphisms restricted to subsets of non-unital rings is a function. (Contributed by AV, 4-Mar-2020.)
|- ( ph -> B = ( U i^i Rng ) )   &    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   =>    |- ( ph -> H Fn ( B X. B ) )
Theorem	rnghmresel 33045	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.)
|- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) /\ F e. ( X H Y ) ) -> F e. ( X RngHomo Y ) )
Theorem	rngcbas 33046	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.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> B = ( U i^i Rng ) )
Theorem	rngchomfval 33047	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.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )
Theorem	rngchom 33048	Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X H Y ) = ( X RngHomo Y ) )
Theorem	elrngchom 33049	A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020.)
|- C = (RngCat ` 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	rngchomfeqhom 33050	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.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> ( Hom f ` C ) = ( Hom ` C ) )
Theorem	rngccofval 33051	Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   =>    |- ( ph -> .x. = (comp ` (ExtStrCat ` U ) ) )
Theorem	rngcco 33052	Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RngCat ` 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	dfrngc2 33053	Alternate definition of the category of non-unital rings (in a universe). (Contributed by AV, 16-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Rng ) )   &    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   &    |- ( ph -> .x. = (comp ` (ExtStrCat ` U ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	rnghmsscmap2 33054*	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.)
|- ( ph -> U e. V )   &    |- ( ph -> R = (Rng i^i U ) )   =>    |- ( ph -> ( RngHomo |` ( R X. R ) ) C_cat ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
Theorem	rnghmsscmap 33055*	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.)
|- ( ph -> U e. V )   &    |- ( ph -> R = (Rng i^i U ) )   =>    |- ( ph -> ( RngHomo |` ( R X. R ) ) C_cat ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
Theorem	rnghmsubcsetclem1 33056	Lemma 1 for rnghmsubcsetc 33058. (Contributed by AV, 9-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = (Rng i^i U ) )   &    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   =>    |- ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )
Theorem	rnghmsubcsetclem2 33057*	Lemma 2 for rnghmsubcsetc 33058. (Contributed by AV, 9-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = (Rng i^i U ) )   &    |- ( ph -> H = ( RngHomo |` ( 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	rnghmsubcsetc 33058	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.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = (Rng i^i U ) )   &    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   =>    |- ( ph -> H e. (Subcat ` C ) )
Theorem	rngccat 33059	The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 9-Mar-2020.)
|- C = (RngCat ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	rngcid 33060	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.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- S = ( Base ` X )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` S ) )
Theorem	rngcsect 33061	A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.)
|- C = (RngCat ` 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 RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( G o. F ) = ( _I |` E ) ) ) )
Theorem	rngcinv 33062	An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.)
|- C = (RngCat ` 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 RngIsom Y ) /\ G = `' F ) ) )
Theorem	rngciso 33063	An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.)
|- C = (RngCat ` 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 RngIsom Y ) ) )
Theorem	rngcbasALTV 33064	Set of objects of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> B = ( U i^i Rng ) )
Theorem	rngchomfvalALTV 33065*	Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( x e. B , y e. B |-> ( x RngHomo y ) ) )
Theorem	rngchomALTV 33066	Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X H Y ) = ( X RngHomo Y ) )
Theorem	elrngchomALTV 33067	A morphism of non-unital rings is a function. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` 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	rngccofvalALTV 33068*	Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` 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 ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) )
Theorem	rngccoALTV 33069	Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` 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 RngHomo Y ) )   &    |- ( ph -> G e. ( Y RngHomo Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )
Theorem	rngccatidALTV 33070*	Lemma for rngccatALTV 33071. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` U )   &    |- B = ( Base ` C )   =>    |- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( _I |` ( Base ` x ) ) ) ) )
Theorem	rngccatALTV 33071	The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatALTV ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	rngcidALTV 33072	The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatALTV ` U )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- S = ( Base ` X )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` S ) )
Theorem	rngcsectALTV 33073	A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatALTV ` 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 RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( G o. F ) = ( _I |` E ) ) ) )
Theorem	rngcinvALTV 33074	An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatALTV ` 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 RngIsom Y ) /\ G = `' F ) ) )
Theorem	rngcisoALTV 33075	An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatALTV ` 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 RngIsom Y ) ) )
Theorem	rngchomffvalALTV 33076*	The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) in maps-to notation for an operation. (Contributed by AV, 1-Mar-2020.) (New usage is discouraged.)
|- C = (RngCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- F = ( Hom f ` C )   =>    |- ( ph -> F = ( x e. B , y e. B |-> ( x RngHomo y ) ) )
Theorem	rngchomrnghmresALTV 33077	The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) as restriction of the non-unital ring homomorphisms. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
|- C = (RngCatALTV ` U )   &    |- B = (Rng i^i U )   &    |- ( ph -> U e. V )   &    |- F = ( Hom f ` C )   =>    |- ( ph -> F = ( RngHomo |` ( B X. B ) ) )
Theorem	rngcifuestrc 33078*	The "inclusion functor" from the category of non-unital rings into the category of extensible structures. (Contributed by AV, 30-Mar-2020.)
|- R = (RngCat ` U )   &    |- E = (ExtStrCat ` U )   &    |- B = ( Base ` R )   &    |- ( ph -> U e. V )   &    |- ( ph -> F = ( _I |` B ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RngHomo y ) ) ) )   =>    |- ( ph -> F ( R Func E ) G )
Theorem	funcrngcsetc 33079*	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 33080, using cofuval2 15378 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 33078, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 15620. (Contributed by AV, 26-Mar-2020.)
|- R = (RngCat ` 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 RngHomo y ) ) ) )   =>    |- ( ph -> F ( R Func S ) G )
Theorem	funcrngcsetcALT 33080*	Alternate proof of funcrngcsetc 33079, using cofuval2 15378 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 33078, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 15620. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 33079. (Contributed by AV, 30-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- R = (RngCat ` 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 RngHomo y ) ) ) )   =>    |- ( ph -> F ( R Func S ) G )
Theorem	zrinitorngc 33081	The zero ring is an initial object in the category of nonunital 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. (InitO ` C ) )
Theorem	zrtermorngc 33082	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 33083	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 ) )
21.24.10.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 33086. Alternatively, 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 33099. 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 33092, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom |` ( B X. B ) ), see ringchomfval 33093, whereas the composition is the ordinary composition of functions, see ringccofval 33097 and ringcco 33098. 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 33101, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 33104. It follows that the category of rings RingCat is actually a category, see ringccat 33105 with the identity function as identity arrow, see ringcid 33106. 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 33107, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 33110. 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 33111: ( (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 33116.
Syntax	cringc 33084	Extend class notation to include the category Ring.
class RingCat
Syntax	cringcALTV 33085	Extend class notation to include the category Ring. (New usage is discouraged.)
class RingCatALTV
Definition	df-ringc 33086	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 33087*	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 33088*	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 33089	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 33090	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 33091	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 33092	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 33093	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 33094	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 33095	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 33096	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 33097	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 33098	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 33099	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 33100*	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 ) ) ) )