P. 135 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13401-13500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	imasaddf 13401*	The image structure's group operation is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   =>    |- ( ph -> .xb : ( B X. B ) --> B )
Theorem	imasmulfn 13402*	The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ph -> .xb Fn ( B X. B ) )
Theorem	imasmulval 13403*	The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Theorem	imasmulf 13404*	The image structure's ring multiplication is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   =>    |- ( ph -> .xb : ( B X. B ) --> B )
Theorem	qusval 13405*	Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> U = ( F "s R ) )
Theorem	quslem 13406*	The function in qusval 13405 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> F : V -onto-> ( V /. .~ ) )
Theorem	qusex 13407	Existence of a quotient structure. (Contributed by Jim Kingdon, 25-Apr-2025.)
|- ( ( R e. V /\ .~ e. W ) -> ( R /.s .~ ) e. _V )
Theorem	qusin 13408	Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( .~ " V ) C_ V )   =>    |- ( ph -> U = ( R /.s ( .~ i^i ( V X. V ) ) ) )
Theorem	qusbas 13409	Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> ( V /. .~ ) = ( Base ` U ) )
Theorem	divsfval 13410*	Value of the function in qusval 13405. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   =>    |- ( ph -> ( F ` A ) = [ A ] .~ )
Theorem	divsfvalg 13411*	Value of the function in qusval 13405. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( F ` A ) = [ A ] .~ )
Theorem	ercpbllemg 13412*	Lemma for ercpbl 13413. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   =>    |- ( ph -> ( ( F ` A ) = ( F ` B ) <-> A .~ B ) )
Theorem	ercpbl 13413*	Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( a .+ b ) e. V )   &    |- ( ph -> ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) ) )   =>    |- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( F ` ( A .+ B ) ) = ( F ` ( C .+ D ) ) ) )
Theorem	erlecpbl 13414*	Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> ( ( A .~ C /\ B .~ D ) -> ( A N B <-> C N D ) ) )   =>    |- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( A N B <-> C N D ) ) )
Theorem	qusaddvallemg 13415*	Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   &    |- ( ph -> .x. e. W )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
Theorem	qusaddflemg 13416*	The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   &    |- ( ph -> .x. e. W )   =>    |- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )
Theorem	qusaddval 13417*	The addition in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
Theorem	qusaddf 13418*	The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   =>    |- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )
Theorem	qusmulval 13419*	The multiplication in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
Theorem	qusmulf 13420*	The multiplication in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )
Theorem	fnpr2o 13421	Function with a domain of 2o. (Contributed by Jim Kingdon, 25-Sep-2023.)
|- ( ( A e. V /\ B e. W ) -> { <. (/) , A >. , <. 1o , B >. } Fn 2o )
Theorem	fnpr2ob 13422	Biconditional version of fnpr2o 13421. (Contributed by Jim Kingdon, 27-Sep-2023.)
|- ( ( A e. _V /\ B e. _V ) <-> { <. (/) , A >. , <. 1o , B >. } Fn 2o )
Theorem	fvpr0o 13423	The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.)
|- ( A e. V -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A )
Theorem	fvpr1o 13424	The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.)
|- ( B e. V -> ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) = B )
Theorem	fvprif 13425	The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( ( A e. V /\ B e. W /\ C e. 2o ) -> ( { <. (/) , A >. , <. 1o , B >. } ` C ) = if ( C = (/) , A , B ) )
Theorem	xpsfrnel 13426*	Elementhood in the target space of the function F appearing in xpsval 13434. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( G e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( G Fn 2o /\ ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) )
Theorem	xpsfeq 13427	A function on 2o is determined by its values at zero and one. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- ( G Fn 2o -> { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } = G )
Theorem	xpsfrnel2 13428*	Elementhood in the target space of the function F appearing in xpsval 13434. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- ( { <. (/) , X >. , <. 1o , Y >. } e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( X e. A /\ Y e. B ) )
Theorem	xpscf 13429	Equivalent condition for the pair function to be a proper function on A. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( { <. (/) , X >. , <. 1o , Y >. } : 2o --> A <-> ( X e. A /\ Y e. A ) )
Theorem	xpsfval 13430*	The value of the function appearing in xpsval 13434. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } )   =>    |- ( ( X e. A /\ Y e. B ) -> ( X F Y ) = { <. (/) , X >. , <. 1o , Y >. } )
Theorem	xpsff1o 13431*	The function appearing in xpsval 13434 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = { (/) , 1o }. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } )   =>    |- F : ( A X. B ) -1-1-onto-> X_ k e. 2o if ( k = (/) , A , B )
Theorem	xpsfrn 13432*	A short expression for the indexed cartesian product on two indices. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } )   =>    |- ran F = X_ k e. 2o if ( k = (/) , A , B )
Theorem	xpsff1o2 13433*	The function appearing in xpsval 13434 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = { (/) , 1o }. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } )   =>    |- F : ( A X. B ) -1-1-onto-> ran F
Theorem	xpsval 13434*	Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)
|- T = ( R X.s S )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   &    |- F = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )   &    |- G = (Scalar ` R )   &    |- U = ( G X_s { <. (/) , R >. , <. 1o , S >. } )   =>    |- ( ph -> T = ( `' F "s U ) )
PART 7  BASIC ALGEBRAIC STRUCTURES
7.1  Monoids
7.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-mpo 6022, binary operations are defined by a rule, and with df-ov 6020, 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 6020 (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 6020). The definition of magmas (Mgm, see df-mgm 13438) 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 13435	Extend class notation with group addition as a function.
class +f
Syntax	cmgm 13436	Extend class notation with class of all magmas.
class Mgm
Definition	df-plusf 13437*	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 13448), while +g only has closure (mgmcl 13441). (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 13438*	A magma is a set equipped with an everywhere defined internal operation. Definition 1 in [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 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 13439*	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 13440*	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 13441	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 13442	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	mgmsscl 13443	If the base set of a magma is contained in the base set of another magma, and the group operation of the magma is the restriction of the group operation of the other magma to its base set, then the base set of the magma is closed under the group operation of the other magma. (Contributed by AV, 17-Feb-2024.)
|- B = ( Base ` G )   &    |- S = ( Base ` H )   =>    |- ( ( ( G e. Mgm /\ H e. Mgm ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) /\ ( X e. S /\ Y e. S ) ) -> ( X ( +g ` G ) Y ) e. S )
Theorem	plusffvalg 13444*	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 2-Mar-2024.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( G e. V -> .+^ = ( x e. B , y e. B |-> ( x .+ y ) ) )
Theorem	plusfvalg 13445	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( ( G e. V /\ X e. B /\ Y e. B ) -> ( X .+^ Y ) = ( X .+ Y ) )
Theorem	plusfeqg 13446	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 )   =>    |- ( ( G e. V /\ .+ Fn ( B X. B ) ) -> .+^ = .+ )
Theorem	plusffng 13447	The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.)
|- B = ( Base ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( G e. V -> .+^ Fn ( B X. B ) )
Theorem	mgmplusf 13448	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 13449	The internal operation for a set is the trivial operation iff the set is a singleton. (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 13450	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	mgm0 13451	Any set with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021.)
|- ( ( M e. V /\ ( Base ` M ) = (/) ) -> M e. Mgm )
Theorem	mgm1 13452	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	opifismgmdc 13453*	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 /\ ( x e. B /\ y e. B ) ) -> DECID ps )   &    |- ( ph -> E. x x e. 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 )
7.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 13454) is an important property of monoids, and therefore also for groups, but also for magmas not required to be associative. Magmas with 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 13340. Related theorems which are already valid for magmas are provided in the following.
Theorem	mgmidmo 13454*	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	grpidvalg 13455*	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 )   =>    |- ( G e. V -> .0. = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) ) )
Theorem	grpidpropdg 13456*	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 -> K e. V )   &    |- ( ph -> L e. W )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( 0g ` K ) = ( 0g ` L ) )
Theorem	fn0g 13457	The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- 0g Fn _V
Theorem	0g0 13458	The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015.)
|- (/) = ( 0g ` (/) )
Theorem	ismgmid 13459*	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 13460*	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 13461*	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 13462*	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	lidrideqd 13463*	If there is a left and right identity element for any binary operation (group operation) .+, both identity elements are equal. Generalization of statement in [Lang] p. 3: it is sufficient that "e" is a left identity element and "e`" is a right identity element instead of both being (two-sided) identity elements. (Contributed by AV, 26-Dec-2023.)
|- ( ph -> L e. B )   &    |- ( ph -> R e. B )   &    |- ( ph -> A. x e. B ( L .+ x ) = x )   &    |- ( ph -> A. x e. B ( x .+ R ) = x )   =>    |- ( ph -> L = R )
Theorem	lidrididd 13464*	If there is a left and right identity element for any binary operation (group operation) .+, the left identity element (and therefore also the right identity element according to lidrideqd 13463) is equal to the two-sided identity element. (Contributed by AV, 26-Dec-2023.)
|- ( ph -> L e. B )   &    |- ( ph -> R e. B )   &    |- ( ph -> A. x e. B ( L .+ x ) = x )   &    |- ( ph -> A. x e. B ( x .+ R ) = x )   &    |- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ph -> L = .0. )
Theorem	grpidd 13465*	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	mgmidsssn0 13466*	Property 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. } )
Theorem	grpinvalem 13467*	Lemma for grpinva 13468. (Contributed by NM, 9-Aug-2013.)
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ph -> O e. B )   &    |- ( ( ph /\ x e. B ) -> ( O .+ x ) = x )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O )   &    |- ( ( ph /\ ps ) -> X e. B )   &    |- ( ( ph /\ ps ) -> ( X .+ X ) = X )   =>    |- ( ( ph /\ ps ) -> X = O )
Theorem	grpinva 13468*	Deduce right inverse from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ph -> O e. B )   &    |- ( ( ph /\ x e. B ) -> ( O .+ x ) = x )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O )   &    |- ( ( ph /\ ps ) -> X e. B )   &    |- ( ( ph /\ ps ) -> N e. B )   &    |- ( ( ph /\ ps ) -> ( N .+ X ) = O )   =>    |- ( ( ph /\ ps ) -> ( X .+ N ) = O )
Theorem	grprida 13469*	Deduce right identity from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ph -> O e. B )   &    |- ( ( ph /\ x e. B ) -> ( O .+ x ) = x )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O )   =>    |- ( ( ph /\ x e. B ) -> ( x .+ O ) = x )
7.1.3  Iterated sums in a magma The symbol gsumg is mostly used in the context of abelian groups. Therefore, it is usually called "group sum". It can be defined, however, in arbitrary magmas (then it should be called "iterated sum"). If the magma is not required to be commutative or associative, then the order of the summands and the order in which summations are done become important. If the magma is not unital, then one cannot define a meaningful empty sum. See the comment for df-igsum 13341.
Theorem	fngsum 13470	Iterated sum has a universal domain. (Contributed by Jim Kingdon, 28-Jun-2025.)
|- gsumg Fn ( _V X. _V )
Theorem	igsumvalx 13471*	Expand out the substitutions in df-igsum 13341. (Contributed by Mario Carneiro, 18-Sep-2015.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> F e. X )   &    |- ( ph -> dom F = A )   =>    |- ( ph -> ( G gsumg F ) = ( iota x ( ( A = (/) /\ x = .0. ) \/ E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) ) )
Theorem	igsumval 13472*	Expand out the substitutions in df-igsum 13341. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> A e. X )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( G gsumg F ) = ( iota x ( ( A = (/) /\ x = .0. ) \/ E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) ) )
Theorem	gsumfzval 13473	An expression for gsumg when summing over a finite set of sequential integers. (Contributed by Jim Kingdon, 14-Aug-2025.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( G gsumg F ) = if ( N < M , .0. , ( seq M ( .+ , F ) ` N ) ) )
Theorem	gsumpropd 13474	The group sum depends only on the base set and additive operation. (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	gsumpropd2 13475*	A stronger version of gsumpropd 13474, working for magma, where only the closure of the addition operation on a common base is required, see gsummgmpropd 13476. (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 13476*	A stronger version of gsumpropd 13474 if at least one of the involved structures is a magma, see gsumpropd2 13475. (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 13477*	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	gsum0g 13478	Value of the empty group sum. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- .0. = ( 0g ` G )   =>    |- ( G e. V -> ( G gsumg (/) ) = .0. )
Theorem	gsumval2 13479	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	gsumsplit1r 13480	Splitting off the rightmost summand of a group sum. This corresponds to the (inductive) definition of a (finite) product in [Lang] p. 4, first formula. (Contributed by AV, 26-Dec-2023.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... ( N + 1 ) ) --> B )   =>    |- ( ph -> ( G gsumg F ) = ( ( G gsumg ( F |` ( M ... N ) ) ) .+ ( F ` ( N + 1 ) ) ) )
Theorem	gsumprval 13481	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 13482	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 ) ) )
7.1.4  Semigroups A semigroup (Smgrp, see df-sgrp 13484) is a set together with an associative binary operation (see Wikipedia, Semigroup, 8-Jan-2020, https://en.wikipedia.org/wiki/Semigroup 13484). In other words, a semigroup is an associative magma. The notion of semigroup is a generalization of that of group where the existence of an identity or inverses is not required.
Syntax	csgrp 13483	Extend class notation with class of all semigroups.
class Smgrp
Definition	df-sgrp 13484*	A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 13438), whose operation is associative. Definition in section II.1 of [Bruck] p. 23, or of an "associative magma" in definition 5 of [BourbakiAlg1] p. 4 . (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- Smgrp = { 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 13485*	The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( M e. Smgrp <-> ( 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 13486*	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. Smgrp <-> 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 13487*	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. Smgrp <-> 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 13488	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/ Smgrp ) )
Theorem	sgrpmgm 13489	A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- ( M e. Smgrp -> M e. Mgm )
Theorem	sgrpass 13490	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. Smgrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) )
Theorem	sgrpcl 13491	Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025.)
|- B = ( Base ` G )   &    |- .o. = ( +g ` G )   =>    |- ( ( G e. Smgrp /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B )
Theorem	sgrp0 13492	Any set with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021.)
|- ( ( M e. V /\ ( Base ` M ) = (/) ) -> M e. Smgrp )
Theorem	sgrp1 13493	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. Smgrp )
Theorem	issgrpd 13494*	Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> G e. V )   =>    |- ( ph -> G e. Smgrp )
Theorem	sgrppropd 13495*	If two structures are sets, have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a semigroup iff the other one is. (Contributed by AV, 15-Feb-2025.)
|- ( ph -> K e. V )   &    |- ( ph -> L e. W )   &    |- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( K e. Smgrp <-> L e. Smgrp ) )
Theorem	prdsplusgsgrpcl 13496	Structure product pointwise sums are closed when the factors are semigroups. (Contributed by AV, 21-Feb-2025.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R : I -->Smgrp )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( F .+ G ) e. B )
Theorem	prdssgrpd 13497	The product of a family of semigroups is a semigroup. (Contributed by AV, 21-Feb-2025.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I -->Smgrp )   =>    |- ( ph -> Y e. Smgrp )
7.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 13499, 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 13501. 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 13498	Extend class notation with class of all monoids.
class Mnd
Definition	df-mnd 13499*	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 13505), whose operation is associative (see mndass 13506) and has a two-sided neutral element (see mndid 13507), see also ismnd 13501. (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
|- Mnd = { g e. Smgrp | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x ) }
Theorem	ismnddef 13500*	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. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )