P. 396 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39501-39600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rngdir 39501	Distributive law for the multiplication operation of a nonunital ring (right-distributivity). (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )
Theorem	rngcl 39502	Closure of the multiplication operation of a nonunital ring. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
Theorem	rnglz 39503	The zero of a nonunital ring is a left-absorbing element. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Rng /\ X e. B ) -> ( .0. .x. X ) = .0. )
21.33.13.3  Rng homomorphisms
Syntax	crngh 39504	non-unital ring homomorphisms.
class RngHomo
Syntax	crngs 39505	non-unital ring isomorphisms.
class RngIsom
Definition	df-rnghomo 39506*	Define the set of non-unital ring homomorphisms from r to s. (Contributed by AV, 20-Feb-2020.)
|- RngHomo = ( r e. Rng , s e. Rng |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) } )
Definition	df-rngisom 39507*	Define the set of non-unital ring isomorphisms from r to s. (Contributed by AV, 20-Feb-2020.)
|- RngIsom = ( r e. _V , s e. _V |-> { f e. ( r RngHomo s ) | `' f e. ( s RngHomo r ) } )
Theorem	rnghmrcl 39508	Reverse closure of a non-unital ring homomorphism. (Contributed by AV, 22-Feb-2020.)
|- ( F e. ( R RngHomo S ) -> ( R e. Rng /\ S e. Rng ) )
Theorem	rnghmfn 39509	The mapping of two non-unital rings to the non-unital ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.)
|- RngHomo Fn (Rng X. Rng )
Theorem	rnghmval 39510*	The set of the non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 22-Feb-2020.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .* = ( .r ` S )   &    |- C = ( Base ` S )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` S )   =>    |- ( ( R e. Rng /\ S e. Rng ) -> ( R RngHomo S ) = { f e. ( C ^m B ) | A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )
Theorem	isrnghm 39511*	A function is a non-unital ring homomorphism iff it is a group homomorphism and preserves multiplication. (Contributed by AV, 22-Feb-2020.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .* = ( .r ` S )   =>    |- ( F e. ( R RngHomo S ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) )
Theorem	isrnghmmul 39512	A function is a non-unital ring homomorphism iff it preserves both addition and multiplication. (Contributed by AV, 27-Feb-2020.)
|- M = (mulGrp ` R )   &    |- N = (mulGrp ` S )   =>    |- ( F e. ( R RngHomo S ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ F e. ( M MgmHom N ) ) ) )
Theorem	rnghmmgmhm 39513	A non-unital ring homomorphism is a homomorphism of multiplicative magmas. (Contributed by AV, 27-Feb-2020.)
|- M = (mulGrp ` R )   &    |- N = (mulGrp ` S )   =>    |- ( F e. ( R RngHomo S ) -> F e. ( M MgmHom N ) )
Theorem	rnghmval2 39514	The non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 1-Mar-2020.)
|- ( ( R e. Rng /\ S e. Rng ) -> ( R RngHomo S ) = ( ( R GrpHom S ) i^i ( (mulGrp ` R ) MgmHom (mulGrp ` S ) ) ) )
Theorem	isrngisom 39515	An isomorphism of non-unital rings is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Feb-2020.)
|- ( ( R e. V /\ S e. W ) -> ( F e. ( R RngIsom S ) <-> ( F e. ( R RngHomo S ) /\ `' F e. ( S RngHomo R ) ) ) )
Theorem	rngimrcl 39516	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 39517	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 39518	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 39519	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 39520*	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 39521*	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 39522	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 39523	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 39524	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 39525	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 39526	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 39527	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 39528*	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 39529*	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 39530*	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 39531*	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 39532*	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 39533*	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 39534*	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 39535*	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 39536*	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 39537	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 39538	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 39539	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 39540*	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 39541	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 39542	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 39543	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 39544	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 39545	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 39546	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 39547	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 39548	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 39549	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 39550*	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 39551*	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 39552*	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 39553*	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 39554*	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 39434. (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 39555*	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 39556*	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 39557*	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 39558*	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 39559*	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 39560*	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 39561*	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 39562*	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 39563*	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 39564*	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 39565*	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 39566*	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 39567*	The ring of integers restricted to the even integers is a (non-unital) ring, the "ring of even integers". Alternate version of 2zrng 39554, 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 39563) and a multiplicative semigroup (see 2zrngmsgrp 39566). (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 39568*	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 39569*	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 39570*	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 39571*	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 39572	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 39573	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 39574	Lemma for cznrng 39576: 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 39575	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 39576*	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 39577*	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 39580. 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 39581 or dfrngc2 39593. 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 39586, 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 39587, whereas the composition is the ordinary composition of functions, see rngccofval 39591 and rngcco 39592. 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 39595, 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 39598. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 39599 with the identity function as identity arrow, see rngcid 39600.
Syntax	crngc 39578	Extend class notation to include the category Rng.
class RngCat
Syntax	crngcALTV 39579	Extend class notation to include the category Rng. (New usage is discouraged.)
class RngCatALTV
Definition	df-rngc 39580	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 39581*	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 39582*	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 39583	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 39584	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 39585	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 39586	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 39587	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 39588	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 39589	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 39590	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 39591	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 39592	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 39593	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 39594*	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 39595*	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 39596	Lemma 1 for rnghmsubcsetc 39598. (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 39597*	Lemma 2 for rnghmsubcsetc 39598. (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 39598	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 39599	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 39600	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 ) )