P. 401 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40001-40100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rngimrcl 40001	Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020.)
|- ( F e. ( R RngIsom S ) -> ( R e. _V /\ S e. _V ) )
Theorem	rnghmghm 40002	A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020.)
|- ( F e. ( R RngHomo S ) -> F e. ( R GrpHom S ) )
Theorem	rnghmf 40003	A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R RngHomo S ) -> F : B --> C )
Theorem	rnghmmul 40004	A homomorphism of non-unital rings preserves multiplication. (Contributed by AV, 23-Feb-2020.)
|- X = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` S )   =>    |- ( ( F e. ( R RngHomo S ) /\ A e. X /\ B e. X ) -> ( F ` ( A .x. B ) ) = ( ( F ` A ) .X. ( F ` B ) ) )
Theorem	isrnghm2d 40005*	Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` S )   &    |- ( ph -> R e. Rng )   &    |- ( ph -> S e. Rng )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )   &    |- ( ph -> F e. ( R GrpHom S ) )   =>    |- ( ph -> F e. ( R RngHomo S ) )
Theorem	isrnghmd 40006*	Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` S )   &    |- ( ph -> R e. Rng )   &    |- ( ph -> S e. Rng )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )   &    |- C = ( Base ` S )   &    |- .+ = ( +g ` R )   &    |- .+^ = ( +g ` S )   &    |- ( ph -> F : B --> C )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   =>    |- ( ph -> F e. ( R RngHomo S ) )
Theorem	rnghmf1o 40007	A non-unital ring homomorphism is bijective iff its converse is also a non-unital ring homomorphism. (Contributed by AV, 27-Feb-2020.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R RngHomo S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S RngHomo R ) ) )
Theorem	isrngim 40008	An isomorphism of non-unital rings is a bijective homomorphism. (Contributed by AV, 23-Feb-2020.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( ( R e. V /\ S e. W ) -> ( F e. ( R RngIsom S ) <-> ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) ) )
Theorem	rngimf1o 40009	An isomorphism of non-unital rings is a bijection. (Contributed by AV, 23-Feb-2020.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R RngIsom S ) -> F : B -1-1-onto-> C )
Theorem	rngimrnghm 40010	An isomorphism of non-unital rings is a homomorphism. (Contributed by AV, 23-Feb-2020.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R RngIsom S ) -> F e. ( R RngHomo S ) )
Theorem	rnghmco 40011	The composition of non-unital ring homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.)
|- ( ( F e. ( T RngHomo U ) /\ G e. ( S RngHomo T ) ) -> ( F o. G ) e. ( S RngHomo U ) )
Theorem	idrnghm 40012	The identity homomorphism on a non-unital ring. (Contributed by AV, 27-Feb-2020.)
|- B = ( Base ` R )   =>    |- ( R e. Rng -> ( _I |` B ) e. ( R RngHomo R ) )
Theorem	c0mgm 40013*	The constant mapping to zero is a magma homomorphism into a monoid. Remark: Instead of the assumption that T is a monoid, it would be sufficient that T is a magma with a right or left identity. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` S )   &    |- .0. = ( 0g ` T )   &    |- H = ( x e. B |-> .0. )   =>    |- ( ( S e. Mgm /\ T e. Mnd ) -> H e. ( S MgmHom T ) )
Theorem	c0mhm 40014*	The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-Apr-2020.)
|- B = ( Base ` S )   &    |- .0. = ( 0g ` T )   &    |- H = ( x e. B |-> .0. )   =>    |- ( ( S e. Mnd /\ T e. Mnd ) -> H e. ( S MndHom T ) )
Theorem	c0ghm 40015*	The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020.)
|- B = ( Base ` S )   &    |- .0. = ( 0g ` T )   &    |- H = ( x e. B |-> .0. )   =>    |- ( ( S e. Grp /\ T e. Grp ) -> H e. ( S GrpHom T ) )
Theorem	c0rhm 40016*	The constant mapping to zero is a ring homomorphism from any ring to the zero ring. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` S )   &    |- .0. = ( 0g ` T )   &    |- H = ( x e. B |-> .0. )   =>    |- ( ( S e. Ring /\ T e. ( Ring \ NzRing ) ) -> H e. ( S RingHom T ) )
Theorem	c0rnghm 40017*	The constant mapping to zero is a nonunital ring homomorphism from any nonunital ring to the zero ring. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` S )   &    |- .0. = ( 0g ` T )   &    |- H = ( x e. B |-> .0. )   =>    |- ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> H e. ( S RngHomo T ) )
Theorem	c0snmgmhm 40018*	The constant mapping to zero is a magma homomorphism from a magma with one element to any monoid. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` T )   &    |- .0. = ( 0g ` S )   &    |- H = ( x e. B |-> .0. )   =>    |- ( ( S e. Mnd /\ T e. Mgm /\ ( # ` B ) = 1 ) -> H e. ( T MgmHom S ) )
Theorem	c0snmhm 40019*	The constant mapping to zero is a monoid homomorphism from the trivial monoid (consisting of the zero only) to any monoid. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` T )   &    |- .0. = ( 0g ` S )   &    |- H = ( x e. B |-> .0. )   &    |- Z = ( 0g ` T )   =>    |- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> H e. ( T MndHom S ) )
Theorem	c0snghm 40020*	The constant mapping to zero is a group homomorphism from the trivial group (consisting of the zero only) to any group. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` T )   &    |- .0. = ( 0g ` S )   &    |- H = ( x e. B |-> .0. )   &    |- Z = ( 0g ` T )   =>    |- ( ( S e. Grp /\ T e. Grp /\ B = { Z } ) -> H e. ( T GrpHom S ) )
Theorem	zrrnghm 40021*	The constant mapping to zero is a nonunital ring homomorphism from the zero ring to any nonunital ring. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` T )   &    |- .0. = ( 0g ` S )   &    |- H = ( x e. B |-> .0. )   =>    |- ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> H e. ( T RngHomo S ) )
21.33.13.4  Ring homomorphisms (extension)
Theorem	rhmfn 40022	The mapping of two rings to the ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.)
|- RingHom Fn ( Ring X. Ring )
Theorem	rhmval 40023	The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.)
|- ( ( R e. Ring /\ S e. Ring ) -> ( R RingHom S ) = ( ( R GrpHom S ) i^i ( (mulGrp ` R ) MndHom (mulGrp ` S ) ) ) )
Theorem	rhmisrnghm 40024	Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020.)
|- ( F e. ( R RingHom S ) -> F e. ( R RngHomo S ) )
21.33.13.5  Ideals as non-unital rings
Theorem	lidldomn1 40025*	If a (left) ideal (which is not the zero ideal) of a domain has a multiplicative identity element, the identity element is the identity of the domain. (Contributed by AV, 17-Feb-2020.)
|- L = (LIdeal ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> ( A. x e. U ( ( I .x. x ) = x /\ ( x .x. I ) = x ) -> I = .1. ) )
Theorem	lidlssbas 40026	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 40027	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 40028	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 40029	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 40030	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 40031	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 40032	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 40033	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 40034	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.33.13.6  The non-unital ring of even integers
Theorem	0even 40035*	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 40036*	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 40037*	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 40038*	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 40039*	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 39919. (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 40040*	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 40041*	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 40042*	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 40043*	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 40044*	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 40045*	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 40046*	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 40047*	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 40048*	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 40049*	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 40050*	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 40051*	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 40052*	The ring of integers restricted to the even integers is a (non-unital) ring, the "ring of even integers". Alternate version of 2zrng 40039, 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 40048) and a multiplicative semigroup (see 2zrngmsgrp 40051). (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 40053*	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 40054*	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 40055*	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 40056*	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.33.13.7  A constructed not unital ring
Theorem	plusgndxnmulrndx 40057	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 40058	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 40059	Lemma for cznrng 40061: 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 40060	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 40061*	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 40062*	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.33.13.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 40065. 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 40066 or dfrngc2 40078. 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 40071, 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 40072, whereas the composition is the ordinary composition of functions, see rngccofval 40076 and rngcco 40077. 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 40080, 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 40083. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 40084 with the identity function as identity arrow, see rngcid 40085.
Syntax	crngc 40063	Extend class notation to include the category Rng.
class RngCat
Syntax	crngcALTV 40064	Extend class notation to include the category Rng. (New usage is discouraged.)
class RngCatALTV
Definition	df-rngc 40065	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 40066*	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 40067*	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 40068	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 40069	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 40070	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 40071	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 40072	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 40073	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 40074	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 40075	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 40076	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 40077	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 40078	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 40079*	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 40080*	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 40081	Lemma 1 for rnghmsubcsetc 40083. (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 40082*	Lemma 2 for rnghmsubcsetc 40083. (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 40083	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 40084	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 40085	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 40086	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 40087	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 40088	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 40089	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 40090*	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 40091	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 40092	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 40093*	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 40094	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 40095*	Lemma for rngccatALTV 40096. (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 40096	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 40097	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 40098	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 40099	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 40100	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 ) ) )