P. 128 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12701-12800   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-pws 12701*	Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
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 5875, binary operations are defined by a rule, and with df-ov 5873, 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 5873 (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 5873). The definition of magmas (Mgm, see df-mgm 12705) 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 12702	Extend class notation with group addition as a function.
class +f
Syntax	cmgm 12703	Extend class notation with class of all magmas.
class Mgm
Definition	df-plusf 12704*	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 12715), while +g only has closure (mgmcl 12708). (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 12705*	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 12706*	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 12707*	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 12708	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 12709	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 12710	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 12711*	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 12712	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 12713	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 12714	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 12715	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 12716	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 12717	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 12718	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 12719	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 12720*	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 12721) 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 12693. Related theorems which are already valid for magmas are provided in the following.
Theorem	mgmidmo 12721*	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 12722*	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 12723*	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 12724	The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- 0g Fn _V
Theorem	0g0 12725	The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015.)
|- (/) = ( 0g ` (/) )
Theorem	ismgmid 12726*	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 12727*	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 12728*	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 12729*	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 12730*	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 12731*	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 12730) 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 12732*	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 12733*	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	grprinvlem 12734*	Lemma for grprinvd 12735. (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	grprinvd 12735*	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	grpridd 12736*	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  Semigroups A semigroup (Smgrp, see df-sgrp 12738) is a set together with an associative binary operation (see Wikipedia, Semigroup, 8-Jan-2020, https://en.wikipedia.org/wiki/Semigroup 12738). 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 12737	Extend class notation with class of all semigroups.
class Smgrp
Definition	df-sgrp 12738*	A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 12705), 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 12739*	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 12740*	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 12741*	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 12742	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 12743	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 12744	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	sgrp0 12745	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 12746	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 )
7.1.4  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 12748, 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 12750. 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 12747	Extend class notation with class of all monoids.
class Mnd
Definition	df-mnd 12748*	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 12754), whose operation is associative (see mndass 12755) and has a two-sided neutral element (see mndid 12756), see also ismnd 12750. (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 12749*	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 ) ) )
Theorem	ismnd 12750*	The predicate "is a monoid". This is the defining 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 12754), whose operation is associative (so, a semigroup, see also mndass 12755) and has a two-sided neutral element (see mndid 12756). (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 ) ) )
Theorem	sgrpidmndm 12751*	A semigroup with an identity element which is inhabited is a monoid. Of course there could be monoids with the empty set as identity element, but these cannot be proven to be monoids with this theorem. (Contributed by AV, 29-Jan-2024.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Smgrp /\ E. e e. B ( E. w w e. e /\ e = .0. ) ) -> G e. Mnd )
Theorem	mndsgrp 12752	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. Smgrp )
Theorem	mndmgm 12753	A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) (Proof shortened by AV, 6-Feb-2020.)
|- ( M e. Mnd -> M e. Mgm )
Theorem	mndcl 12754	Closure of the operation of a monoid. (Contributed by NM, 14-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Proof shortened by AV, 8-Feb-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
Theorem	mndass 12755	A monoid operation is associative. (Contributed by NM, 14-Aug-2011.) (Proof shortened by AV, 8-Feb-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
Theorem	mndid 12756*	A monoid has a two-sided identity element. (Contributed by NM, 16-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Mnd -> E. u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) )
Theorem	mndideu 12757*	The two-sided identity element of a monoid is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by Mario Carneiro, 8-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Mnd -> E! u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) )
Theorem	mnd32g 12758	Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> ( Y .+ Z ) = ( Z .+ Y ) )   =>    |- ( ph -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Z ) .+ Y ) )
Theorem	mnd12g 12759	Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> ( X .+ Y ) = ( Y .+ X ) )   =>    |- ( ph -> ( X .+ ( Y .+ Z ) ) = ( Y .+ ( X .+ Z ) ) )
Theorem	mnd4g 12760	Commutative/associative law for commutative monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> W e. B )   &    |- ( ph -> ( Y .+ Z ) = ( Z .+ Y ) )   =>    |- ( ph -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( ( X .+ Z ) .+ ( Y .+ W ) ) )
Theorem	mndidcl 12761	The identity element of a monoid belongs to the monoid. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Mnd -> .0. e. B )
Theorem	mndbn0 12762	The base set of a monoid is not empty. (It is also inhabited, as seen at mndidcl 12761). Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.)
|- B = ( Base ` G )   =>    |- ( G e. Mnd -> B =/= (/) )
Theorem	hashfinmndnn 12763	A finite monoid has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> (♯ ` B ) e. NN )
Theorem	mndplusf 12764	The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 3-Feb-2020.)
|- B = ( Base ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( G e. Mnd -> .+^ : ( B X. B ) --> B )
Theorem	mndlrid 12765	A monoid's identity element is a two-sided identity. (Contributed by NM, 18-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Mnd /\ X e. B ) -> ( ( .0. .+ X ) = X /\ ( X .+ .0. ) = X ) )
Theorem	mndlid 12766	The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Mnd /\ X e. B ) -> ( .0. .+ X ) = X )
Theorem	mndrid 12767	The identity element of a monoid is a right identity. (Contributed by NM, 18-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Mnd /\ X e. B ) -> ( X .+ .0. ) = X )
Theorem	ismndd 12768*	Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( 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 -> .0. e. B )   &    |- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )   &    |- ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x )   =>    |- ( ph -> G e. Mnd )
Theorem	mndpfo 12769	The addition operation of a monoid as a function is an onto function. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 11-Oct-2013.) (Revised by AV, 23-Jan-2020.)
|- B = ( Base ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( G e. Mnd -> .+^ : ( B X. B ) -onto-> B )
Theorem	mndfo 12770	The addition operation of a monoid is an onto function (assuming it is a function). (Contributed by Mario Carneiro, 11-Oct-2013.) (Proof shortened by AV, 23-Jan-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) -onto-> B )
Theorem	mndpropd 12771*	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, one is a monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( 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. Mnd <-> L e. Mnd ) )
Theorem	mndprop 12772	If two structures have the same group components (properties), one is a monoid iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.)
|- ( Base ` K ) = ( Base ` L )   &    |- ( +g ` K ) = ( +g ` L )   =>    |- ( K e. Mnd <-> L e. Mnd )
Theorem	issubmnd 12773*	Characterize a submonoid by closure properties. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- H = ( G ↾s S )   =>    |- ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) -> ( H e. Mnd <-> A. x e. S A. y e. S ( x .+ y ) e. S ) )
Theorem	mndinvmod 12774*	Uniqueness of an inverse element in a monoid, if it exists. (Contributed by AV, 20-Jan-2024.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. B )   =>    |- ( ph -> E* w e. B ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) )
Theorem	mnd1 12775	The (smallest) structure representing a trivial monoid consists of one element. (Contributed by AV, 28-Apr-2019.) (Proof shortened by AV, 11-Feb-2020.)
|- M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }   =>    |- ( I e. V -> M e. Mnd )
Theorem	mnd1id 12776	The singleton element of a trivial monoid is its identity element. (Contributed by AV, 23-Jan-2020.)
|- M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }   =>    |- ( I e. V -> ( 0g ` M ) = I )
7.1.5  Monoid homomorphisms and submonoids
Syntax	cmhm 12777	Hom-set generator class for monoids.
class MndHom
Syntax	csubmnd 12778	Class function taking a monoid to its lattice of submonoids.
class SubMnd
Definition	df-mhm 12779*	A monoid homomorphism is a function on the base sets which preserves the binary operation and the identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- MndHom = ( s e. Mnd , t e. Mnd |-> { f e. ( ( Base ` t ) ^m ( Base ` s ) ) | ( A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) ) } )
Definition	df-submnd 12780*	A submonoid is a subset of a monoid which contains the identity and is closed under the operation. Such subsets are themselves monoids with the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- SubMnd = ( s e. Mnd |-> { t e. ~P ( Base ` s ) | ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t ) } )
Theorem	ismhm 12781*	Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- 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 : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) ) )
Theorem	mhmrcl1 12782	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- ( F e. ( S MndHom T ) -> S e. Mnd )
Theorem	mhmrcl2 12783	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- ( F e. ( S MndHom T ) -> T e. Mnd )
Theorem	mhmf 12784	A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- B = ( Base ` S )   &    |- C = ( Base ` T )   =>    |- ( F e. ( S MndHom T ) -> F : B --> C )
Theorem	mhmpropd 12785*	Monoid homomorphism depends only on the monoidal attributes of structures. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 7-Nov-2015.)
|- ( ph -> B = ( Base ` J ) )   &    |- ( ph -> C = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> C = ( Base ` M ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )   =>    |- ( ph -> ( J MndHom K ) = ( L MndHom M ) )
Theorem	mhmlin 12786	A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- B = ( Base ` S )   &    |- .+ = ( +g ` S )   &    |- .+^ = ( +g ` T )   =>    |- ( ( F e. ( S MndHom T ) /\ X e. B /\ Y e. B ) -> ( F ` ( X .+ Y ) ) = ( ( F ` X ) .+^ ( F ` Y ) ) )
Theorem	mhm0 12787	A monoid homomorphism preserves zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- .0. = ( 0g ` S )   &    |- Y = ( 0g ` T )   =>    |- ( F e. ( S MndHom T ) -> ( F ` .0. ) = Y )
Theorem	idmhm 12788	The identity homomorphism on a monoid. (Contributed by AV, 14-Feb-2020.)
|- B = ( Base ` M )   =>    |- ( M e. Mnd -> ( _I |` B ) e. ( M MndHom M ) )
Theorem	mhmf1o 12789	A monoid homomorphism is bijective iff its converse is also a monoid homomorphism. (Contributed by AV, 22-Oct-2019.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R MndHom S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S MndHom R ) ) )
Theorem	submrcl 12790	Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- ( S e. (SubMnd ` M ) -> M e. Mnd )
Theorem	issubm 12791*	Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- B = ( Base ` M )   &    |- .0. = ( 0g ` M )   &    |- .+ = ( +g ` M )   =>    |- ( M e. Mnd -> ( S e. (SubMnd ` M ) <-> ( S C_ B /\ .0. e. S /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) )
Theorem	issubm2 12792	Submonoids are subsets that are also monoids with the same zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- B = ( Base ` M )   &    |- .0. = ( 0g ` M )   &    |- H = ( M ↾s S )   =>    |- ( M e. Mnd -> ( S e. (SubMnd ` M ) <-> ( S C_ B /\ .0. e. S /\ H e. Mnd ) ) )
Theorem	issubmd 12793*	Deduction for proving a submonoid. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   &    |- .0. = ( 0g ` M )   &    |- ( ph -> M e. Mnd )   &    |- ( ph -> ch )   &    |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( th /\ ta ) ) ) -> et )   &    |- ( z = .0. -> ( ps <-> ch ) )   &    |- ( z = x -> ( ps <-> th ) )   &    |- ( z = y -> ( ps <-> ta ) )   &    |- ( z = ( x .+ y ) -> ( ps <-> et ) )   =>    |- ( ph -> { z e. B | ps } e. (SubMnd ` M ) )
Theorem	mndissubm 12794	If the base set of a monoid is contained in the base set of another monoid, and the group operation of the monoid is the restriction of the group operation of the other monoid to its base set, and the identity element of the the other monoid is contained in the base set of the monoid, then the (base set of the) monoid is a submonoid of the other monoid. (Contributed by AV, 17-Feb-2024.)
|- B = ( Base ` G )   &    |- S = ( Base ` H )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Mnd /\ H e. Mnd ) -> ( ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> S e. (SubMnd ` G ) ) )
Theorem	submss 12795	Submonoids are subsets of the base set. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- B = ( Base ` M )   =>    |- ( S e. (SubMnd ` M ) -> S C_ B )
Theorem	submid 12796	Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- B = ( Base ` M )   =>    |- ( M e. Mnd -> B e. (SubMnd ` M ) )
Theorem	subm0cl 12797	Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- .0. = ( 0g ` M )   =>    |- ( S e. (SubMnd ` M ) -> .0. e. S )
Theorem	submcl 12798	Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- .+ = ( +g ` M )   =>    |- ( ( S e. (SubMnd ` M ) /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )
Theorem	0subm 12799	The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.)
|- .0. = ( 0g ` G )   =>    |- ( G e. Mnd -> { .0. } e. (SubMnd ` G ) )
Theorem	insubm 12800	The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.)
|- ( ( A e. (SubMnd ` M ) /\ B e. (SubMnd ` M ) ) -> ( A i^i B ) e. (SubMnd ` M ) )