P. 419 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41801-41900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mgmhmco 41801	The composition of magma homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.)
|- ( ( F e. ( T MgmHom U ) /\ G e. ( S MgmHom T ) ) -> ( F o. G ) e. ( S MgmHom U ) )
Theorem	mgmhmima 41802	The homomorphic image of a submagma is a submagma. (Contributed by AV, 27-Feb-2020.)
|- ( ( F e. ( M MgmHom N ) /\ X e. (SubMgm ` M ) ) -> ( F " X ) e. (SubMgm ` N ) )
Theorem	mgmhmeql 41803	The equalizer of two magma homomorphisms is a submagma. (Contributed by AV, 27-Feb-2020.)
|- ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) -> dom ( F i^i G ) e. (SubMgm ` S ) )
Theorem	submgmacs 41804	Submagmas are an algebraic closure system. (Contributed by AV, 27-Feb-2020.)
|- B = ( Base ` G )   =>    |- ( G e. Mgm -> (SubMgm ` G ) e. (ACS ` B ) )
Theorem	ismhm0 41805	Property of a monoid homomorphism, expressed by a magma homomorphism. (Contributed by AV, 17-Apr-2020.)
|- B = ( Base ` S )   &    |- C = ( Base ` T )   &    |- .+ = ( +g ` S )   &    |- .+^ = ( +g ` T )   &    |- .0. = ( 0g ` S )   &    |- Y = ( 0g ` T )   =>    |- ( F e. ( S MndHom T ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( F e. ( S MgmHom T ) /\ ( F ` .0. ) = Y ) ) )
Theorem	mhmismgmhm 41806	Each monoid homomorphism is a magma homomorphism. (Contributed by AV, 29-Feb-2020.)
|- ( F e. ( R MndHom S ) -> F e. ( R MgmHom S ) )
20.35.11.4  Examples and counterexamples for magmas, semigroups and monoids (extension)
Theorem	opmpt2ismgm 41807*	A structure with a group addition operation in maps-to notation is a magma if the operation value is contained in the base set. (Contributed by AV, 16-Feb-2020.)
|- B = ( Base ` M )   &    |- ( +g ` M ) = ( x e. B , y e. B |-> C )   &    |- ( ph -> B =/= (/) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> C e. B )   =>    |- ( ph -> M e. Mgm )
Theorem	copissgrp 41808*	A structure with a constant group addition operation is a semigroup if the constant is contained in the base set. (Contributed by AV, 16-Feb-2020.)
|- B = ( Base ` M )   &    |- ( +g ` M ) = ( x e. B , y e. B |-> C )   &    |- ( ph -> B =/= (/) )   &    |- ( ph -> C e. B )   =>    |- ( ph -> M e. SGrp )
Theorem	copisnmnd 41809*	A structure with a constant group addition operation and at least two elements is not a monoid. (Contributed by AV, 16-Feb-2020.)
|- B = ( Base ` M )   &    |- ( +g ` M ) = ( x e. B , y e. B |-> C )   &    |- ( ph -> C e. B )   &    |- ( ph -> 1 < ( # ` B ) )   =>    |- ( ph -> M e/ Mnd )
Theorem	0nodd 41810*	0 is not an odd integer. (Contributed by AV, 3-Feb-2020.)
|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }   =>    |- 0 e/ O
Theorem	1odd 41811*	1 is an odd integer. (Contributed by AV, 3-Feb-2020.)
|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }   =>    |- 1 e. O
Theorem	2nodd 41812*	2 is not an odd integer. (Contributed by AV, 3-Feb-2020.)
|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }   =>    |- 2 e/ O
Theorem	oddibas 41813*	Lemma 1 for oddinmgm 41815: The base set of M is the set of all odd integers. (Contributed by AV, 3-Feb-2020.)
|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }   &    |- M = (ℂfld ↾s O )   =>    |- O = ( Base ` M )
Theorem	oddiadd 41814*	Lemma 2 for oddinmgm 41815: The group addition operation of M is the addition of complex numbers. (Contributed by AV, 3-Feb-2020.)
|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }   &    |- M = (ℂfld ↾s O )   =>    |- + = ( +g ` M )
Theorem	oddinmgm 41815*	The structure of all odd integers together with the addition of complex numbers is not a magma. Remark: the structure of the complementary subset of the set of integers, the even integers, is a magma, actually an abelian group, see 2zrngaabl 41944, and even a non-unital ring, see 2zrng 41935. (Contributed by AV, 3-Feb-2020.)
|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }   &    |- M = (ℂfld ↾s O )   =>    |- M e/ Mgm
Theorem	nnsgrpmgm 41816	The structure of positive integers together with the addition of complex numbers is a magma. (Contributed by AV, 4-Feb-2020.)
|- M = (ℂfld ↾s NN )   =>    |- M e. Mgm
Theorem	nnsgrp 41817	The structure of positive integers together with the addition of complex numbers is a semigroup. (Contributed by AV, 4-Feb-2020.)
|- M = (ℂfld ↾s NN )   =>    |- M e. SGrp
Theorem	nnsgrpnmnd 41818	The structure of positive integers together with the addition of complex numbers is not a monoid. (Contributed by AV, 4-Feb-2020.)
|- M = (ℂfld ↾s NN )   =>    |- M e/ Mnd
20.35.12  Magmas and internal binary operations (alternate approach) With df-mpt2 6655, binary operations are defined by a rule, and with df-ov 6653, the value of a binary operation applied to two operands can be expressed. In both cases, the two operands can belong to different sets, and the result can be an element of a third set. However, according to Wikipedia "Binary operation", see https://en.wikipedia.org/wiki/Binary_operation (19-Jan-2020), "... a binary operation on a set S is a mapping of the elements of the Cartesian product S X. S to S: f : S X. S --> S. Because the result of performing the operation on a pair of elements of S is again an element of S, the operation is called a closed binary operation on S (or sometimes expressed as having the property of closure).". To distinguish this more restrictive definition (in Wikipedia and most of the literature) from the general case, we call binary operations mapping the elements of the Cartesian product S X. S internal binary operations, see df-intop 41835. If, in addition, the result is also contained in the set S, the operation is called closed internal binary operation, see df-clintop 41836. Therefore, a "binary operation on a set S" according to Wikipedia is a "closed internal binary operation" in our terminology. If the sets are different, the operation is explicitly called external binary operation (see Wikipedia https://en.wikipedia.org/wiki/Binary_operation#External_binary_operations ). Taking a step back, we define "laws" applicable for "binary operations" (which even need not to be functions), according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7. These laws are used, on the one hand, to specialize internal binary operations (see df-clintop 41836 and df-assintop 41837), and on the other hand to define the common algebraic structures like magmas, groups, rings, etc. Internal binary operations, which obey these laws, are defined afterwards. Notice that in [BourbakiAlg1] p. 1, p. 4 and p. 7, these operations are called "laws" by themselves. In the following, an alternate definition df-cllaw 41822 for an internal binary operation is provided, which does not require function-ness, but only closure. Therefore, this definition could be used as binary operation (Slot 2) defined for a magma as extensible structure, see mgmplusgiopALT 41830, or for an alternate definition df-mgm2 41855 for a magma as extensible structure. Similar results are obtained for an associative operation (defining semigroups).
20.35.12.1  Laws for internal binary operations In this subsection, the "laws" applicable for "binary operations" according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7 are defined. These laws are called "internal laws" in [BourbakiAlg1] p. xxi.
Syntax	ccllaw 41819	Extend class notation for the closure law.
class clLaw
Syntax	casslaw 41820	Extend class notation for the associative law.
class assLaw
Syntax	ccomlaw 41821	Extend class notation for the commutative law.
class comLaw
Definition	df-cllaw 41822*	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 41823*	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 41824*	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 41825*	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 41826*	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 41827	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 41828*	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 41829*	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 41830	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 41831	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 ) )
20.35.12.2  Internal binary operations In this subsection, "internal binary operations" obeying different laws are defined.
Syntax	cintop 41832	Extend class notation with class of internal (binary) operations for a set.
class intOp
Syntax	cclintop 41833	Extend class notation with class of closed operations for a set.
class clIntOp
Syntax	cassintop 41834	Extend class notation with class of associative operations for a set.
class assIntOp
Definition	df-intop 41835*	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 41836	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 41837*	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 41838	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 41839	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 41840	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 41841*	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 41842*	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 41843	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 41844	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 41845	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 41846*	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 41847	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 41848	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 41849	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 41850*	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 ) ) )
20.35.12.3  Alternative definitions for Magmas and Semigroups
Syntax	cmgm2 41851	Extend class notation with class of all magmas.
class MgmALT
Syntax	ccmgm2 41852	Extend class notation with class of all commutative magmas.
class CMgmALT
Syntax	csgrp2 41853	Extend class notation with class of all semigroups.
class SGrpALT
Syntax	ccsgrp2 41854	Extend class notation with class of all commutative semigroups.
class CSGrpALT
Definition	df-mgm2 41855	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 41856	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 41857	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 41858	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 41859	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 41860	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 41861	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 41862	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 41863	Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.)
|- ( M e. MgmALT <-> M e. Mgm )
Theorem	sgrp2sgrp 41864	Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.)
|- ( M e. SGrpALT <-> M e. SGrp )
20.35.13  Categories (extension)
20.35.13.1  Subcategories (extension)
Theorem	idfusubc0 41865*	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 41866*	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 41867*	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 )
20.35.14  Rings (extension)
20.35.14.1  Nonzero rings (extension)
Theorem	lmod0rng 41868	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 41869	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 41870	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 41871	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 41872	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 41873	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 ) = (/) )
20.35.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 41874	Extend class notation with class of all non-unital rings.
class Rng
Definition	df-rng0 41875*	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 41876*	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 41877	A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)
|- ( R e. Rng -> R e. Abel )
Theorem	rngmgp 41878	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 41879	A unital ring is a (non-unital) ring. (Contributed by AV, 6-Jan-2020.)
|- ( R e. Ring -> R e. Rng )
Theorem	ringssrng 41880	The unital rings are (non-unital) rings. (Contributed by AV, 20-Mar-2020.)
|- Ring C_ Rng
Theorem	isringrng 41881*	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 41882	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 41883	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 41884	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. )
20.35.14.3  Rng homomorphisms
Syntax	crngh 41885	non-unital ring homomorphisms.
class RngHomo
Syntax	crngs 41886	non-unital ring isomorphisms.
class RngIsom
Definition	df-rnghomo 41887*	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 41888*	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 41889	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 41890	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 41891*	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 41892*	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 41893	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 41894	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 41895	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 41896	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 41897	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 41898	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 41899	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 41900	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 ) ) )