P. 387 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38601-38700   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cassintop 38601	Extend class notation with class of associative operations for a set.
class assIntOp
Definition	df-intop 38602*	Function mapping a set to the class of all internal (binary) operations for this set. (Contributed by AV, 20-Jan-2020.)
|- intOp = ( m e. _V , n e. _V |-> ( n ^m ( m X. m ) ) )
Definition	df-clintop 38603	Function mapping a set to the class of all closed (internal binary) operations for this set, see definition in section 1.2 of [Hall] p. 2, definition in section I.1 of [Bruck] p. 1, or definition 1 in [BourbakiAlg1] p. 1, where it is called "a law of composition". (Contributed by AV, 20-Jan-2020.)
|- clIntOp = ( m e. _V |-> ( m intOp m ) )
Definition	df-assintop 38604*	Function mapping a set to the class of all associative (closed internal binary) operations for this set, see definition 5 in [BourbakiAlg1] p. 4, where it is called "an associative law of composition". (Contributed by AV, 20-Jan-2020.)
|- assIntOp = ( m e. _V |-> { o e. ( clIntOp ` m ) | o assLaw m } )
Theorem	intopval 38605	The internal (binary) operations for a set. (Contributed by AV, 20-Jan-2020.)
|- ( ( M e. V /\ N e. W ) -> ( M intOp N ) = ( N ^m ( M X. M ) ) )
Theorem	intop 38606	An internal (binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
|- ( .o. e. ( M intOp N ) -> .o. : ( M X. M ) --> N )
Theorem	clintopval 38607	The closed (internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.)
|- ( M e. V -> ( clIntOp ` M ) = ( M ^m ( M X. M ) ) )
Theorem	assintopval 38608*	The associative (closed internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.)
|- ( M e. V -> ( assIntOp ` M ) = { o e. ( clIntOp ` M ) | o assLaw M } )
Theorem	assintopmap 38609*	The associative (closed internal binary) operations for a set, expressed with set exponentiation. (Contributed by AV, 20-Jan-2020.)
|- ( M e. V -> ( assIntOp ` M ) = { o e. ( M ^m ( M X. M ) ) | o assLaw M } )
Theorem	isclintop 38610	The predicate "is a closed (internal binary) operations for a set". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.)
|- ( M e. V -> ( .o. e. ( clIntOp ` M ) <-> .o. : ( M X. M ) --> M ) )
Theorem	clintop 38611	A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
|- ( .o. e. ( clIntOp ` M ) -> .o. : ( M X. M ) --> M )
Theorem	assintop 38612	An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
|- ( .o. e. ( assIntOp ` M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) )
Theorem	isassintop 38613*	The predicate "is an associative (closed internal binary) operations for a set". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.)
|- ( M e. V -> ( .o. e. ( assIntOp ` M ) <-> ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) )
Theorem	clintopcllaw 38614	The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.)
|- ( .o. e. ( clIntOp ` M ) -> .o. clLaw M )
Theorem	assintopcllaw 38615	The closure low holds for an associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.)
|- ( .o. e. ( assIntOp ` M ) -> .o. clLaw M )
Theorem	assintopasslaw 38616	The associative low holds for a associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.)
|- ( .o. e. ( assIntOp ` M ) -> .o. assLaw M )
Theorem	assintopass 38617*	An associative (closed internal binary) operation for a set is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.)
|- ( .o. e. ( assIntOp ` M ) -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) )
21.33.10.3  Alternative definitions for Magmas and Semigroups
Syntax	cmgm2 38618	Extend class notation with class of all magmas.
class MgmALT
Syntax	ccmgm2 38619	Extend class notation with class of all commutative magmas.
class CMgmALT
Syntax	csgrp2 38620	Extend class notation with class of all semigroups.
class SGrpALT
Syntax	ccsgrp2 38621	Extend class notation with class of all commutative semigroups.
class CSGrpALT
Definition	df-mgm2 38622	A magma is a set equipped with a closed operation. Definition 1 of [BourbakiAlg1] p. 1, or definition of a groupoid in section I.1 of [Bruck] p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by AV, 6-Jan-2020.)
|- MgmALT = { m | ( +g ` m ) clLaw ( Base ` m ) }
Definition	df-cmgm2 38623	A commutative magma is a magma with a commutative operation. Definition 8 of [BourbakiAlg1] p. 7. (Contributed by AV, 20-Jan-2020.)
|- CMgmALT = { m e. MgmALT | ( +g ` m ) comLaw ( Base ` m ) }
Definition	df-sgrp2 38624	A semigroup is a magma with an associative operation. Definition in section II.1 of [Bruck] p. 23, or of an "associative magma" in definition 5 of [BourbakiAlg1] p. 4, or of a semi-group in section 1.3 of [Hall] p. 7. (Contributed by AV, 6-Jan-2020.)
|- SGrpALT = { g e. MgmALT | ( +g ` g ) assLaw ( Base ` g ) }
Definition	df-csgrp2 38625	A commutative semigroup is a semigroup with a commutative operation. (Contributed by AV, 20-Jan-2020.)
|- CSGrpALT = { g e. SGrpALT | ( +g ` g ) comLaw ( Base ` g ) }
Theorem	ismgmALT 38626	The predicate "is a magma." (Contributed by AV, 16-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( M e. V -> ( M e. MgmALT <-> .o. clLaw B ) )
Theorem	iscmgmALT 38627	The predicate "is a commutative magma." (Contributed by AV, 20-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( M e. CMgmALT <-> ( M e. MgmALT /\ .o. comLaw B ) )
Theorem	issgrpALT 38628	The predicate "is a semigroup." (Contributed by AV, 16-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( M e. SGrpALT <-> ( M e. MgmALT /\ .o. assLaw B ) )
Theorem	iscsgrpALT 38629	The predicate "is a commutative semigroup." (Contributed by AV, 20-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( M e. CSGrpALT <-> ( M e. SGrpALT /\ .o. comLaw B ) )
Theorem	mgm2mgm 38630	Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.)
|- ( M e. MgmALT <-> M e. Mgm )
Theorem	sgrp2sgrp 38631	Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.)
|- ( M e. SGrpALT <-> M e. SGrp )
21.33.11  Categories (extension)
21.33.11.1  Subcategories (extension)
Theorem	idfusubc0 38632*	The identity functor for a subcategory is an "inclusion functor" from the subcategory into its supercategory. (Contributed by AV, 29-Mar-2020.)
|- S = ( C |`cat J )   &    |- I = (idfunc ` S )   &    |- B = ( Base ` S )   =>    |- ( J e. (Subcat ` C ) -> I = <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x ( Hom ` S ) y ) ) ) >. )
Theorem	idfusubc 38633*	The identity functor for a subcategory is an "inclusion functor" from the subcategory into its supercategory. (Contributed by AV, 29-Mar-2020.)
|- S = ( C |`cat J )   &    |- I = (idfunc ` S )   &    |- B = ( Base ` S )   =>    |- ( J e. (Subcat ` C ) -> I = <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x J y ) ) ) >. )
Theorem	inclfusubc 38634*	The "inclusion functor" from a subcategory of a category into the category itself. (Contributed by AV, 30-Mar-2020.)
|- ( ph -> J e. (Subcat ` C ) )   &    |- S = ( C |`cat J )   &    |- B = ( Base ` S )   &    |- ( ph -> F = ( _I |` B ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x J y ) ) ) )   =>    |- ( ph -> F ( S Func C ) G )
21.33.12  Rings (extension)
21.33.12.1  Nonzero rings (extension)
Theorem	lmod0rng 38635	If the scalar ring of a module is the zero ring, the module is the zero module, i.e. the base set of the module is the singleton consisting of the identity element only. (Contributed by AV, 17-Apr-2019.)
|- ( ( M e. LMod /\ -. (Scalar ` M ) e. NzRing ) -> ( Base ` M ) = { ( 0g ` M ) } )
Theorem	nzrneg1ne0 38636	The additive inverse of the 1 in a nonzero ring is not zero ( -1 =/= 0 ). (Contributed by AV, 29-Apr-2019.)
|- ( R e. NzRing -> ( ( invg ` R ) ` ( 1r ` R ) ) =/= ( 0g ` R ) )
Theorem	0ringdif 38637	A zero ring is a ring which is not a nonzero ring. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. ( Ring \ NzRing ) <-> ( R e. Ring /\ B = { .0. } ) )
Theorem	0ringbas 38638	The base set of a zero ring, a ring which is not a nonzero ring, is the singleton of the zero element. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. ( Ring \ NzRing ) -> B = { .0. } )
Theorem	0ring1eq0 38639	In a zero ring, a ring which is not a nonzero ring, the unit equals the zero element. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. ( Ring \ NzRing ) -> .1. = .0. )
Theorem	nrhmzr 38640	There is no ring homomorphism from the zero ring into a nonzero ring. (Contributed by AV, 18-Apr-2020.)
|- ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> ( Z RingHom R ) = (/) )
21.33.12.2  Non-unital rings ("rngs") According to Wikipedia, "... in abstract algebra, a rng (or pseudo-ring or non-unital ring) is an algebraic structure satisfying the same properties as a [unital] ring, without assuming the existence of a multiplicative identity. The term "rng" (pronounced rung) is meant to suggest that it is a "ring" without "i", i.e. without the requirement for an "identity element"." (see https://en.wikipedia.org/wiki/Rng_(algebra), 6-Jan-2020).
Syntax	crng 38641	Extend class notation with class of all non-unital rings.
class Rng
Definition	df-rng0 38642*	Define class of all (non-unital) rings. A non-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of [BourbakiAlg1] p. 93 or the definition of a ring in part Preliminaries of [Roman] p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020.)
|- Rng = { f e. Abel | ( (mulGrp ` f ) e. SGrp /\ [. ( Base ` f ) / b ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) }
Theorem	isrng 38643*	The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.)
|- B = ( Base ` R )   &    |- G = (mulGrp ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Rng <-> ( R e. Abel /\ G e. SGrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
Theorem	rngabl 38644	A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
|- ( R e. Rng -> R e. Abel )
Theorem	rngmgp 38645	A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.)
|- G = (mulGrp ` R )   =>    |- ( R e. Rng -> G e. SGrp )
Theorem	ringrng 38646	A unital ring is a (non-unital) ring. (Contributed by AV, 6-Jan-2020.)
|- ( R e. Ring -> R e. Rng )
Theorem	ringssrng 38647	The unital rings are (non-unital) rings. (Contributed by AV, 20-Mar-2020.)
|- Ring C_ Rng
Theorem	isringrng 38648*	The predicate "is a unital ring" as extension of the predicate "is a non-unital ring". (Contributed by AV, 17-Feb-2020.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Ring <-> ( R e. Rng /\ E. x e. B A. y e. B ( ( x .x. y ) = y /\ ( y .x. x ) = y ) ) )
Theorem	rngdir 38649	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 38650	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 38651	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.12.3  Rng homomorphisms
Syntax	crngh 38652	non-unital ring homomorphisms.
class RngHomo
Syntax	crngs 38653	non-unital ring isomorphisms.
class RngIsom
Definition	df-rnghomo 38654*	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 38655*	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 38656	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 38657	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 38658*	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 38659*	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 38660	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 38661	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 38662	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 38663	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 38664	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 38665	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 38666	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 38667	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 38668*	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 38669*	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 38670	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 38671	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 38672	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 38673	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 38674	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 38675	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 38676*	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 38677*	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 38678*	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 38679*	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 38680*	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 38681*	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 38682*	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 38683*	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 38684*	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.12.4  Ring homomorphisms (extension)
Theorem	rhmfn 38685	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 38686	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 38687	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.12.5  Ideals as non-unital rings
Theorem	lidldomn1 38688*	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 38689	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 38690	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 38691	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 38692	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 38693	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 38694	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 38695	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 38696	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 38697	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.12.6  The non-unital ring of even integers
Theorem	0even 38698*	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 38699*	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 38700*	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