P. 158 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15701-15800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dlatjmdi 15701	In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   =>    |- ( ( K e. DLat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ ( Y ./\ Z ) ) = ( ( X .\/ Y ) ./\ ( X .\/ Z ) ) )
9.2.6  Posets and lattices as relations
Syntax	cps 15702	Extend class notation with the class of all posets.
class PosetRel
Syntax	ctsr 15703	Extend class notation with the class of all totally ordered sets.
class TosetRel
Definition	df-ps 15704	Define the class of all posets (partially ordered sets) with weak ordering (e.g. "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric. (Contributed by NM, 11-May-2008.)
|- PosetRel = { r | ( Rel r /\ ( r o. r ) C_ r /\ ( r i^i `' r ) = ( _I |` U. U. r ) ) }
Definition	df-tsr 15705	Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009.)
|- TosetRel = { r e. PosetRel | ( dom r X. dom r ) C_ ( r u. `' r ) }
Theorem	isps 15706	The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008.)
|- ( R e. A -> ( R e. PosetRel <-> ( Rel R /\ ( R o. R ) C_ R /\ ( R i^i `' R ) = ( _I |` U. U. R ) ) ) )
Theorem	psrel 15707	A poset is a relation. (Contributed by NM, 12-May-2008.)
|- ( A e. PosetRel -> Rel A )
Theorem	psref2 15708	A poset is antisymmetric and reflexive. (Contributed by FL, 3-Aug-2009.)
|- ( R e. PosetRel -> ( R i^i `' R ) = ( _I |` U. U. R ) )
Theorem	pstr2 15709	A poset is transitive. (Contributed by FL, 3-Aug-2009.)
|- ( R e. PosetRel -> ( R o. R ) C_ R )
Theorem	pslem 15710	Lemma for psref 15712 and others. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- ( R e. PosetRel -> ( ( ( A R B /\ B R C ) -> A R C ) /\ ( A e. U. U. R -> A R A ) /\ ( ( A R B /\ B R A ) -> A = B ) ) )
Theorem	psdmrn 15711	The domain and range of a poset equal its field. (Contributed by NM, 13-May-2008.)
|- ( R e. PosetRel -> ( dom R = U. U. R /\ ran R = U. U. R ) )
Theorem	psref 15712	A poset is reflexive. (Contributed by NM, 13-May-2008.)
|- X = dom R   =>    |- ( ( R e. PosetRel /\ A e. X ) -> A R A )
Theorem	psrn 15713	The range of a poset equals it domain. (Contributed by NM, 7-Jul-2008.)
|- X = dom R   =>    |- ( R e. PosetRel -> X = ran R )
Theorem	psasym 15714	A poset is antisymmetric. (Contributed by NM, 12-May-2008.)
|- ( ( R e. PosetRel /\ A R B /\ B R A ) -> A = B )
Theorem	pstr 15715	A poset is transitive. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- ( ( R e. PosetRel /\ A R B /\ B R C ) -> A R C )
Theorem	cnvps 15716	The converse of a poset is a poset. In the general case ( `' R e. PosetRel -> R e. PosetRel ) is not true. See cnvpsb 15717 for a special case where the property holds. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 3-Sep-2015.)
|- ( R e. PosetRel -> `' R e. PosetRel )
Theorem	cnvpsb 15717	The converse of a poset is a poset. (Contributed by FL, 5-Jan-2009.)
|- ( Rel R -> ( R e. PosetRel <-> `' R e. PosetRel ) )
Theorem	psss 15718	Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010.)
|- ( R e. PosetRel -> ( R i^i ( A X. A ) ) e. PosetRel )
Theorem	psssdm2 15719	Field of a subposet. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   =>    |- ( R e. PosetRel -> dom ( R i^i ( A X. A ) ) = ( X i^i A ) )
Theorem	psssdm 15720	Field of a subposet. (Contributed by FL, 19-Sep-2011.) (Revised by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. PosetRel /\ A C_ X ) -> dom ( R i^i ( A X. A ) ) = A )
Theorem	istsr 15721	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- X = dom R   =>    |- ( R e. TosetRel <-> ( R e. PosetRel /\ ( X X. X ) C_ ( R u. `' R ) ) )
Theorem	istsr2 15722*	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- X = dom R   =>    |- ( R e. TosetRel <-> ( R e. PosetRel /\ A. x e. X A. y e. X ( x R y \/ y R x ) ) )
Theorem	tsrlin 15723	A toset is a linear order. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. TosetRel /\ A e. X /\ B e. X ) -> ( A R B \/ B R A ) )
Theorem	tsrlemax 15724	Two ways of saying a number is less than or equal to the maximum of two others. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A R if ( B R C , C , B ) <-> ( A R B \/ A R C ) ) )
Theorem	tsrps 15725	A toset is a poset. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( R e. TosetRel -> R e. PosetRel )
Theorem	cnvtsr 15726	The converse of a toset is a toset. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( R e. TosetRel -> `' R e. TosetRel )
Theorem	tsrss 15727	Any subset of a totally ordered set is totally ordered. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Nov-2013.)
|- ( R e. TosetRel -> ( R i^i ( A X. A ) ) e. TosetRel )
Theorem	ledm 15728	domain of <_ is RR*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.)
|- RR* = dom <_
Theorem	lern 15729	The range of <_ is RR*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- RR* = ran <_
Theorem	lefld 15730	The field of the 'less or equal to' relationship on the extended real. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.)
|- RR* = U. U. <_
Theorem	letsr 15731	The "less than or equal to" relationship on the extended reals is a toset. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- <_ e. TosetRel
9.2.7  Directed sets, nets
Syntax	cdir 15732	Extend class notation with the class of all directed sets.
class DirRel
Syntax	ctail 15733	Extend class notation with the tail function.
class tail
Definition	df-dir 15734	Define the class of all directed sets/directions. (Contributed by Jeff Hankins, 25-Nov-2009.)
|- DirRel = { r | ( ( Rel r /\ ( _I |` U. U. r ) C_ r ) /\ ( ( r o. r ) C_ r /\ ( U. U. r X. U. U. r ) C_ ( `' r o. r ) ) ) }
Definition	df-tail 15735*	Define the tail function for directed sets. (Contributed by Jeff Hankins, 25-Nov-2009.)
|- tail = ( r e. DirRel |-> ( x e. U. U. r |-> ( r " { x } ) ) )
Theorem	isdir 15736	A condition for a relation to be a direction. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- A = U. U. R   =>    |- ( R e. V -> ( R e. DirRel <-> ( ( Rel R /\ ( _I |` A ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( A X. A ) C_ ( `' R o. R ) ) ) ) )
Theorem	reldir 15737	A direction is a relation. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- ( R e. DirRel -> Rel R )
Theorem	dirdm 15738	A direction's domain is equal to its field. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- ( R e. DirRel -> dom R = U. U. R )
Theorem	dirref 15739	A direction is reflexive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- X = dom R   =>    |- ( ( R e. DirRel /\ A e. X ) -> A R A )
Theorem	dirtr 15740	A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- ( ( ( R e. DirRel /\ C e. V ) /\ ( A R B /\ B R C ) ) -> A R C )
Theorem	dirge 15741*	For any two elements of a directed set, there exists a third element greater than or equal to both. (Note that this does not say that the two elements have a least upper bound.) (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- X = dom R   =>    |- ( ( R e. DirRel /\ A e. X /\ B e. X ) -> E. x e. X ( A R x /\ B R x ) )
Theorem	tsrdir 15742	A totally ordered set is a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- ( A e. TosetRel -> A e. DirRel )
PART 10  BASIC ALGEBRAIC STRUCTURES
10.1  Monoids
10.1.1  Magmas According to Wikipedia ("Magma (algebra)", 08-Jan-2020, https://en.wikipedia.org/wiki/magma_(algebra)) "In abstract algebra, a magma [...] is a basic kind of algebraic structure. Specifically, a magma consists of a set equipped with a single binary operation. The binary operation must be closed by definition but no other properties are imposed.". Since the concept of a "binary operation" is used in different variants, these differences are explained in more detail in the following: With df-mpt2 6300, binary operations are defined by a rule, and with df-ov 6298, 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, binary operations mapping the elements of the Cartesian product S X. S are more precisely called internal binary operations. If, in addition, the result is also contained in the set S, the operation should be called closed internal binary operation. Therefore, a "binary operation on a set S" according to Wikipedia is a "closed internal binary operation" in a more precise 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 ). The definition of magmas (Mgm, see df-mgm 15746) concentrates on the closure property of the associated operation, and poses no additional restrictions on it. In this way, it is most general and flexible.
Syntax	cplusf 15743	Extend class notation with group addition as a function.
class +f
Syntax	cmgm 15744	Extend class notation with class of all magmas.
class Mgm
Definition	df-plusf 15745*	Define group addition function. Usually we will use +g directly instead of +f, and they have the same behavior in most cases. The main advantage of +f for any magma is that it is a guaranteed function (mgmplusf 15755), while +g only has closure (mgmcl 15749). (Contributed by Mario Carneiro, 14-Aug-2015.)
|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
Definition	df-mgm 15746*	A magma is a set equipped with an everywhere defined internal operation. Definition of a magma in [BourbakiAlg1] p. 1, or of a groupoid in [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 FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
Theorem	ismgm 15747*	The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )
Theorem	ismgmn0 15748*	The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( A e. B -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )
Theorem	mgmcl 15749	Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( ( M e. Mgm /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B )
Theorem	isnmgm 15750	A condition for a structure not to be a magma. (Contributed by AV, 30-Jan-2020.) (Proof shortened by NM, 5-Feb-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( ( X e. B /\ Y e. B /\ ( X .o. Y ) e/ B ) -> M e/ Mgm )
Theorem	plusffval 15751*	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +f ` G )   =>    |- .+^ = ( x e. B , y e. B |-> ( x .+ y ) )
Theorem	plusfval 15752	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( ( X e. B /\ Y e. B ) -> ( X .+^ Y ) = ( X .+ Y ) )
Theorem	plusfeq 15753	If the addition operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( .+ Fn ( B X. B ) -> .+^ = .+ )
Theorem	plusffn 15754	The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.)
|- B = ( Base ` G )   &    |- .+^ = ( +f ` G )   =>    |- .+^ Fn ( B X. B )
Theorem	mgmplusf 15755	The group addition function of a magma is a function into its base set. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revisd by AV, 28-Jan-2020.)
|- B = ( Base ` M )   &    |- .+^ = ( +f ` M )   =>    |- ( M e. Mgm -> .+^ : ( B X. B ) --> B )
Theorem	intopsn 15756	The internal operation for a set is the trivial operation iff the set is a singleton. Formerly part of proof of ring1zr 17793. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 23-Jan-2020.)
|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) )
Theorem	mgmb1mgm1 15757	The only magma with a base set consisting of one element is the trivial magma (at least if its operation is an internal binary operation). (Contributed by AV, 23-Jan-2020.) (Revised by AV, 7-Feb-2020.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   =>    |- ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) )
Theorem	mgm1 15758	The structure with one element and the only closed internal operation for a singleton is a magma. (Contributed by AV, 10-Feb-2020.)
|- M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }   =>    |- ( I e. V -> M e. Mgm )
Theorem	opifismgm 15759*	A structure with a group addition operation expressed by a conditional operator is a magma if both values of the conditional operator are contained in the base set. (Contributed by AV, 9-Feb-2020.)
|- B = ( Base ` M )   &    |- ( +g ` M ) = ( x e. B , y e. B |-> if ( ps , C , D ) )   &    |- ( ph -> B =/= (/) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> C e. B )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> D e. B )   =>    |- ( ph -> M e. Mgm )
10.1.2  Identity elements According to Wikipedia ("Identity element", 7-Feb-2020, https://en.wikipedia.org/wiki/Identity_element): "In mathematics, an identity element, or neutral element, is a special type of element of a set with respect to a binary operation on that set, which leaves any element of the set unchanged when combined with it.". Or in more detail "... an element e of S is called a left identity if e * a = a for all a in S, and a right identity if a * e = a for all a in S. If e is both a left identity and a right identity, then it is called a two-sided identity, or simply an identity." We concentrate on two-sided identities in the following. The existence of an identity (an identity is unique if it exists, see mgmidmo 15760) is an important property of monoids (see mndid 15806), and therefore also for groups (see grpid 15957), but also for magmas not required to be associative. Non-associative magmas having an identity element are called "unital magmas" (see definition 2 in [BourbakiAlg1] p. 12) or, if the magmas are cancellative, "loops" (see definition in [Bruck] p. 15). In the context of extensible structures, the identity element (of any magma M) is defined as "group identity element" ( 0g ` M ), see df-0g 14714. Related theorems which are already valid for magmas are provided in the following.
Theorem	mgmidmo 15760*	A two-sided identity element is unique (if it exists) in any magma. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by NM, 17-Jun-2017.)
|- E* u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x )
Theorem	grpidval 15761*	The value of the identity element of a group. (Contributed by NM, 20-Aug-2011.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- .0. = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
Theorem	grpidpropd 15762*	If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, they have the same identity element. (Contributed by Mario Carneiro, 27-Nov-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( 0g ` K ) = ( 0g ` L ) )
Theorem	fn0g 15763	The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- 0g Fn _V
Theorem	0g0 15764	The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015.)
|- (/) = ( 0g ` (/) )
Theorem	ismgmid 15765*	The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )   =>    |- ( ph -> ( ( U e. B /\ A. x e. B ( ( U .+ x ) = x /\ ( x .+ U ) = x ) ) <-> .0. = U ) )
Theorem	mgmidcl 15766*	The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )   =>    |- ( ph -> .0. e. B )
Theorem	mgmlrid 15767*	The identity element of a magma, if it exists, is a left and right identity. (Contributed by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )   =>    |- ( ( ph /\ X e. B ) -> ( ( .0. .+ X ) = X /\ ( X .+ .0. ) = X ) )
Theorem	ismgmid2 15768*	Show that a given element is the identity element of a magma. (Contributed by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> U e. B )   &    |- ( ( ph /\ x e. B ) -> ( U .+ x ) = x )   &    |- ( ( ph /\ x e. B ) -> ( x .+ U ) = x )   =>    |- ( ph -> U = .0. )
Theorem	grpidd 15769*	Deduce the identity element of a magma from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> .0. e. B )   &    |- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )   &    |- ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x )   =>    |- ( ph -> .0. = ( 0g ` G ) )
Theorem	gsumvallem1 15770*	Lemma for properties of the set of identities of G. Either G has no identities, and O = (/), or it has one and this identity is unique and identified by the 0g function. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }   =>    |- ( G e. V -> O C_ { .0. } )
10.1.3  Ordered sums in a magma Usually, the symbol gsumg is used in the context of (abelian) groups. Therefore it is called "group sum". It can be used, however, also for magmas, that's why the related theorems are provided in the following. If the magma is either not commutative or not associative or has no identity, special care has to be taken. E.g. the order of the single additions could be important, see remark 2. in the comment for df-gsum 14715.
Theorem	gsumvalx 15771*	Expand out the substitutions in df-gsum 14715. (Contributed by Mario Carneiro, 18-Sep-2015.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- O = { s e. B | A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) }   &    |- ( ph -> W = ( `' F " ( _V \ O ) ) )   &    |- ( ph -> G e. V )   &    |- ( ph -> F e. X )   &    |- ( ph -> dom F = A )   =>    |- ( ph -> ( G gsumg F ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) )
Theorem	gsumval 15772*	Expand out the substitutions in df-gsum 14715. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- O = { s e. B | A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) }   &    |- ( ph -> W = ( `' F " ( _V \ O ) ) )   &    |- ( ph -> G e. V )   &    |- ( ph -> A e. X )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( G gsumg F ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) )
Theorem	gsumpropd 15773	The group sum depends only on the base set and additive operation. Note that for entirely unrestricted functions, there can be dependency on out-of-domain values of the operation, so this is somewhat weaker than mndpropd 15819 etc. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Proof shortened by Mario Carneiro, 18-Sep-2015.)
|- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ph -> H e. X )   &    |- ( ph -> ( Base ` G ) = ( Base ` H ) )   &    |- ( ph -> ( +g ` G ) = ( +g ` H ) )   =>    |- ( ph -> ( G gsumg F ) = ( H gsumg F ) )
Theorem	gsumpropd2lem 15774*	Lemma for gsumpropd2 15775 (Contributed by Thierry Arnoux, 28-Jun-2017.)
|- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ph -> H e. X )   &    |- ( ph -> ( Base ` G ) = ( Base ` H ) )   &    |- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) e. ( Base ` G ) )   &    |- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) = ( s ( +g ` H ) t ) )   &    |- ( ph -> Fun F )   &    |- ( ph -> ran F C_ ( Base ` G ) )   &    |- A = ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) )   &    |- B = ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) )   =>    |- ( ph -> ( G gsumg F ) = ( H gsumg F ) )
Theorem	gsumpropd2 15775*	A stronger version of gsumpropd 15773, working for magma, where only the closure of the addition operation on a common base is required, see gsummgmpropd 15776. (Contributed by Thierry Arnoux, 28-Jun-2017.)
|- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ph -> H e. X )   &    |- ( ph -> ( Base ` G ) = ( Base ` H ) )   &    |- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) e. ( Base ` G ) )   &    |- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) = ( s ( +g ` H ) t ) )   &    |- ( ph -> Fun F )   &    |- ( ph -> ran F C_ ( Base ` G ) )   =>    |- ( ph -> ( G gsumg F ) = ( H gsumg F ) )
Theorem	gsummgmpropd 15776*	A stronger version of gsumpropd 15773 if at least one of the involved structures is a magma, see gsumpropd2 15775. (Contributed by AV, 31-Jan-2020.)
|- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ph -> H e. X )   &    |- ( ph -> ( Base ` G ) = ( Base ` H ) )   &    |- ( ph -> G e. Mgm )   &    |- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) = ( s ( +g ` H ) t ) )   &    |- ( ph -> Fun F )   &    |- ( ph -> ran F C_ ( Base ` G ) )   =>    |- ( ph -> ( G gsumg F ) = ( H gsumg F ) )
Theorem	gsumress 15777*	The group sum in a substructure is the same as the group sum in the original structure. The only requirement on the substructure is that it contain the identity element; neither G nor H need be groups. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- H = ( G ↾s S )   &    |- ( ph -> G e. V )   &    |- ( ph -> A e. X )   &    |- ( ph -> S C_ B )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> .0. e. S )   &    |- ( ( ph /\ x e. B ) -> ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) )   =>    |- ( ph -> ( G gsumg F ) = ( H gsumg F ) )
Theorem	gsumval1 15778*	Value of the group sum operation when every element being summed is an identity of G. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }   &    |- ( ph -> G e. V )   &    |- ( ph -> A e. W )   &    |- ( ph -> F : A --> O )   =>    |- ( ph -> ( G gsumg F ) = .0. )
Theorem	gsum0 15779	Value of the empty group sum. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- .0. = ( 0g ` G )   =>    |- ( G gsumg (/) ) = .0.
Theorem	gsumval2a 15780*	Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) --> B )   &    |- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }   &    |- ( ph -> -. ran F C_ O )   =>    |- ( ph -> ( G gsumg F ) = ( seq M ( .+ , F ) ` N ) )
Theorem	gsumval2 15781	Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( G gsumg F ) = ( seq M ( .+ , F ) ` N ) )
Theorem	gsumprval 15782	Value of the group sum operation over a pair of sequential integers. (Contributed by AV, 14-Dec-2018.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N = ( M + 1 ) )   &    |- ( ph -> F : { M , N } --> B )   =>    |- ( ph -> ( G gsumg F ) = ( ( F ` M ) .+ ( F ` N ) ) )
Theorem	gsumpr12val 15783	Value of the group sum operation over the pair { 1 , 2 }. (Contributed by AV, 14-Dec-2018.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> F : { 1 , 2 } --> B )   =>    |- ( ph -> ( G gsumg F ) = ( ( F ` 1 ) .+ ( F ` 2 ) ) )
10.1.4  Semigroups The definition of semigroups (SGrp, see df-sgrp 15785) is according to Wikipedia ("Semigroup", 8-Jan-2020, https://en.wikipedia.org/wiki/Semigroup) "In mathematics, a semigroup is an algebraic structure consisting of a set together with an associative binary operation. ... Semigroups may be considered a special case of magmas, where the operation is associative, or as a generalization of groups, without requiring the existence of an identity element or inverses.".
Syntax	csgrp 15784	Extend class notation with class of all semigroups.
class SGrp
Definition	df-sgrp 15785*	A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 15746), whose operation is associative. Definition of a semigroup in [Bruck] p. 23, or of an "associative magma" in [BourbakiAlg1] p. 4 . (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- SGrp = { g e. Mgm | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) }
Theorem	issgrp 15786*	The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (Revised by by AV, 6-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( M e. SGrp <-> ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
Theorem	issgrpv 15787*	The predicate "is a semigroup" for a structure which is a set. (Contributed by AV, 1-Feb-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( M e. V -> ( M e. SGrp <-> A. x e. B A. y e. B ( ( x .o. y ) e. B /\ A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) )
Theorem	issgrpn0 15788*	The predicate "is a semigroup" for a structure with a nonempty base set. (Contributed by AV, 1-Feb-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( A e. B -> ( M e. SGrp <-> A. x e. B A. y e. B ( ( x .o. y ) e. B /\ A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) )
Theorem	isnsgrp 15789	A condition for a structure not to be a semigroup. (Contributed by AV, 30-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> M e/ SGrp ) )
Theorem	sgrpmgm 15790	A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- ( M e. SGrp -> M e. Mgm )
Theorem	sgrpass 15791	A semigroup operation is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 30-Jan-2020.)
|- B = ( Base ` G )   &    |- .o. = ( +g ` G )   =>    |- ( ( G e. SGrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) )
Theorem	sgrp1 15792	The structure with one element and the only closed internal operation for a singleton is a semigroup. (Contributed by AV, 10-Feb-2020.)
|- M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }   =>    |- ( I e. V -> M e. SGrp )
10.1.5  Definition and basic properties of monoids According to Wikipedia ("Monoid", https://en.wikipedia.org/wiki/Monoid, 6-Feb-2020,) "In abstract algebra [...] a monoid is an algebraic structure with a single associative binary operation and an identity element. Monoids are semigroups with identity.". In the following, monoids are defined in the second way (as semigroups with identity), see df-mnd 15795, whereas many authors define magmas in the first way (as algebraic structure with a single associative binary operation and an identity element, i.e. without the need of a definition for/knowledge about semigroups), see ismnd 15797. See, for example, the definition in [Lang] p. 3: "A monoid is a set G, with a law of composition which is associative, and having a unit element".
Syntax	cmnd 15793	Extend class notation with class of all monoids.
class Mnd
Syntax	cmndOLD 15794	Extend class notation with class of all monoids.
class MndOLD
Definition	df-mnd 15795*	A monoid is a semigroup, which has a two-sided neutral element. Definition 2 in [BourbakiAlg1] p. 12. In other words (according to the definition in [Lang] p. 3), a monoid is a set equipped with an everywhere defined internal operation (see mndcl 15802), whose operation is associative (see mndass 15803) and has a two-sided neutral element (see mndid 15806), see also ismnd 15797. (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
|- Mnd = { g e. SGrp | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x ) }
Theorem	ismnddef 15796*	The predicate "is a monoid", corresponding 1-to-1 to the definition. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 1-Feb-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Mnd <-> ( G e. SGrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
Theorem	ismnd 15797*	The predicate "is a monoid". This is the definig theorem of a monoid by showing that a set is a monoid if and only if it is a set equipped with a closed, everywhere defined internal operation (so, a magma, see mndcl 15802), whose operation is associative (so, a semigroup, see also mndass 15803) and has a two-sided neutral element (see mndid 15806). (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Mnd <-> ( A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
Definition	df-mndOLD 15798*	Obsolete version of df-mnd 15795 as of 6-Feb-2020. Definition of a monoid. A monoid is a set equipped with an everywhere defined internal operation (so, a magma, see mndcl 15802), whose operation is associative (so, a semigroup, see mndass 15803) and has a two-sided neutral element (see mndid 15806). (Contributed by Mario Carneiro, 6-Jan-2015.) (New usage is discouraged.)
|- MndOLD = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. ( A. x e. b A. y e. b A. z e. b ( ( x p y ) e. b /\ ( ( x p y ) p z ) = ( x p ( y p z ) ) ) /\ E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x ) ) }
Theorem	ismndOLD 15799*	Obsolete version of ismnd 15797 as of 6-Feb-2020. The predicate "is a monoid." (Contributed by Mario Carneiro, 6-Jan-2015.) (New usage is discouraged.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. MndOLD <-> ( A. a e. B A. b e. B A. c e. B ( ( a .+ b ) e. B /\ ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
Theorem	mndsgrp 15800	A monoid is a semigroup. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) (Proof shortened by AV, 6-Feb-2020.)
|- ( G e. Mnd -> G e. SGrp )