P. 390 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38901-39000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	intop 38901	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 38902	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 38903*	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 38904*	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 38905	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 38906	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 38907	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 38908*	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 38909	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 38910	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 38911	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 38912*	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.12.3  Alternative definitions for Magmas and Semigroups
Syntax	cmgm2 38913	Extend class notation with class of all magmas.
class MgmALT
Syntax	ccmgm2 38914	Extend class notation with class of all commutative magmas.
class CMgmALT
Syntax	csgrp2 38915	Extend class notation with class of all semigroups.
class SGrpALT
Syntax	ccsgrp2 38916	Extend class notation with class of all commutative semigroups.
class CSGrpALT
Definition	df-mgm2 38917	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 38918	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 38919	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 38920	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 38921	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 38922	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 38923	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 38924	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 38925	Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.)
|- ( M e. MgmALT <-> M e. Mgm )
Theorem	sgrp2sgrp 38926	Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.)
|- ( M e. SGrpALT <-> M e. SGrp )
21.33.13  Categories (extension)
21.33.13.1  Subcategories (extension)
Theorem	idfusubc0 38927*	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 38928*	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 38929*	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.14  Rings (extension)
21.33.14.1  Nonzero rings (extension)
Theorem	lmod0rng 38930	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 38931	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 38932	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 38933	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 38934	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 38935	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.14.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 38936	Extend class notation with class of all non-unital rings.
class Rng
Definition	df-rng0 38937*	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 38938*	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 38939	A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
|- ( R e. Rng -> R e. Abel )
Theorem	rngmgp 38940	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 38941	A unital ring is a (non-unital) ring. (Contributed by AV, 6-Jan-2020.)
|- ( R e. Ring -> R e. Rng )
Theorem	ringssrng 38942	The unital rings are (non-unital) rings. (Contributed by AV, 20-Mar-2020.)
|- Ring C_ Rng
Theorem	isringrng 38943*	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 38944	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 38945	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 38946	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.14.3  Rng homomorphisms
Syntax	crngh 38947	non-unital ring homomorphisms.
class RngHomo
Syntax	crngs 38948	non-unital ring isomorphisms.
class RngIsom
Definition	df-rnghomo 38949*	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 38950*	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 38951	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 38952	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 38953*	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 38954*	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 38955	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 38956	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 38957	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 38958	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 38959	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 38960	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 38961	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 38962	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 38963*	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 38964*	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 38965	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 38966	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 38967	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 38968	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 38969	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 38970	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 38971*	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 38972*	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 38973*	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 38974*	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 38975*	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 38976*	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 38977*	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 38978*	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 38979*	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.14.4  Ring homomorphisms (extension)
Theorem	rhmfn 38980	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 38981	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 38982	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.14.5  Ideals as non-unital rings
Theorem	lidldomn1 38983*	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 38984	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 38985	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 38986	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 38987	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 38988	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 38989	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 38990	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 38991	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 38992	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.14.6  The non-unital ring of even integers
Theorem	0even 38993*	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 38994*	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 38995*	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 38996*	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 38997*	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 38877. (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 38998*	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 38999*	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 39000*	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 )