P. 330 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32901-33000   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-cllaw 32901*	The closure law for binary operations, see definitions of laws A0. and M0. in section 1.1 of [Hall] p. 1, or definition 1 in [BourbakiAlg1] p. 1: the value of a binary operation applied to two operands of a given sets is an element of this set. By this definition, the closure law is expressed as binary relation: a binary operation is related to a set by clLaw if the closure law holds for this binary operation regarding this set. Note that the binary operation needs not to be a function. (Contributed by AV, 7-Jan-2020.)
|- clLaw = { <. o , m >. | A. x e. m A. y e. m ( x o y ) e. m }
Definition	df-comlaw 32902*	The commutative law for binary operations, see definitions of laws A2. and M2. in section 1.1 of [Hall] p. 1, or definition 8 in [BourbakiAlg1] p. 7: the value of a binary operation applied to two operands equals the value of a binary operation applied to the two operands in reversed order. By this definition, the commutative law is expressed as binary relation: a binary operation is related to a set by comLaw if the commutative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by AV, 7-Jan-2020.)
|- comLaw = { <. o , m >. | A. x e. m A. y e. m ( x o y ) = ( y o x ) }
Definition	df-asslaw 32903*	The associative law for binary operations, see definitions of laws A1. and M1. in section 1.1 of [Hall] p. 1, or definition 5 in [BourbakiAlg1] p. 4: the value of a binary operation applied the value of the binary operation applied to two operands and a third operand equals the value of the binary operation applied to the first operand and the value of the binary operation applied to the second and third operand. By this definition, the associative law is expressed as binary relation: a binary operation is related to a set by assLaw if the associative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.)
|- assLaw = { <. o , m >. | A. x e. m A. y e. m A. z e. m ( ( x o y ) o z ) = ( x o ( y o z ) ) }
Theorem	iscllaw 32904*	The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020.)
|- ( ( .o. e. V /\ M e. W ) -> ( .o. clLaw M <-> A. x e. M A. y e. M ( x .o. y ) e. M ) )
Theorem	iscomlaw 32905*	The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020.)
|- ( ( .o. e. V /\ M e. W ) -> ( .o. comLaw M <-> A. x e. M A. y e. M ( x .o. y ) = ( y .o. x ) ) )
Theorem	clcllaw 32906	Closure of a closed operation. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 21-Jan-2020.)
|- ( ( .o. clLaw M /\ X e. M /\ Y e. M ) -> ( X .o. Y ) e. M )
Theorem	isasslaw 32907*	The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.)
|- ( ( .o. e. V /\ M e. W ) -> ( .o. assLaw M <-> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
Theorem	asslawass 32908*	Associativity of an associative operation. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 21-Jan-2020.)
|- ( .o. assLaw M -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) )
Theorem	mgmplusgiopALT 32909	Slot 2 (group operation) of a magma as extensible structure is a closed operation on the base set. (Contributed by AV, 13-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( M e. Mgm -> ( +g ` M ) clLaw ( Base ` M ) )
Theorem	sgrpplusgaopALT 32910	Slot 2 (group operation) of a semigroup as extensible structure is an associative operation on the base set. (Contributed by AV, 13-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( G e. SGrp -> ( +g ` G ) assLaw ( Base ` G ) )
21.24.8.2  Internal binary operations In this subsection, "internal binary operations" obeying different laws are defined.
Syntax	cintop 32911	Extend class notation with class of internal (binary) operations for a set.
class intOp
Syntax	cclintop 32912	Extend class notation with class of closed operations for a set.
class clIntOp
Syntax	cassintop 32913	Extend class notation with class of associative operations for a set.
class assIntOp
Definition	df-intop 32914*	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 32915	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 32916*	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 32917	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 32918	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 32919	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 32920*	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 32921*	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 32922	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 32923	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 32924	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 32925*	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 32926	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 32927	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 32928	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 32929*	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.24.8.3  Alternative definitions for Magmas and Semigroups
Syntax	cmgm2 32930	Extend class notation with class of all magmas.
class MgmALT
Syntax	ccmgm2 32931	Extend class notation with class of all commutative magmas.
class CMgmALT
Syntax	csgrp2 32932	Extend class notation with class of all semigroups.
class SGrpALT
Syntax	ccsgrp2 32933	Extend class notation with class of all commutative semigroups.
class CSGrpALT
Definition	df-mgm2 32934	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 32935	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 32936	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 32937	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 32938	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 32939	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 32940	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 32941	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 32942	Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.)
|- ( M e. MgmALT <-> M e. Mgm )
Theorem	sgrp2sgrp 32943	Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.)
|- ( M e. SGrpALT <-> M e. SGrp )
21.24.9  Categories (extension)
21.24.9.1  Subcategories (extension)
Theorem	idfusubc0 32944*	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 32945*	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 32946*	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.24.10  Rings (extension)
21.24.10.1  Nonzero rings (extension)
Theorem	lmod0rng 32947	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 32948	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 32949	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 32950	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 32951	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 32952	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.24.10.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 32953	Extend class notation with class of all non-unital rings.
class Rng
Definition	df-rng0 32954*	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 32955*	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 32956	A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
|- ( R e. Rng -> R e. Abel )
Theorem	rngmgp 32957	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 32958	A unital ring is a (non-unital) ring. (Contributed by AV, 6-Jan-2020.)
|- ( R e. Ring -> R e. Rng )
Theorem	ringssrng 32959	The unital rings are (non-unital) rings. (Contributed by AV, 20-Mar-2020.)
|- Ring C_ Rng
Theorem	isringrng 32960*	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 32961	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 32962	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 32963	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.24.10.3  Rng homomorphisms
Syntax	crngh 32964	non-unital ring homomorphisms.
class RngHomo
Syntax	crngs 32965	non-unital ring isomorphisms.
class RngIsom
Definition	df-rnghomo 32966*	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 32967*	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 32968	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 32969	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 32970*	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 32971*	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 32972	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 32973	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 32974	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 32975	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 32976	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 32977	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 32978	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 32979	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 32980*	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 32981*	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 32982	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 32983	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 32984	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 32985	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 32986	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 32987	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 32988*	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 32989*	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 32990*	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 32991*	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 32992*	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 32993*	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 32994*	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 32995*	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 32996*	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.24.10.4  Ring homomorphisms (extension)
Theorem	rhmfn 32997	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 32998	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 32999	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.24.10.5  Ideals as non-unital rings
Theorem	lidldomn1 33000*	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. ) )