P. 129 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12801-12900   *Has distinct variable group(s)

Type	Label	Description
Statement
7.1.3  Semigroups A semigroup (Smgrp, see df-sgrp 12802) is a set together with an associative binary operation (see Wikipedia, Semigroup, 8-Jan-2020, https://en.wikipedia.org/wiki/Semigroup 12802). 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 12801	Extend class notation with class of all semigroups.
class Smgrp
Definition	df-sgrp 12802*	A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 12769), 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 12803*	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 12804*	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 12805*	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 12806	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 12807	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 12808	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 12809	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 12810	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 12812, 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 12814. 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 12811	Extend class notation with class of all monoids.
class Mnd
Definition	df-mnd 12812*	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 12818), whose operation is associative (see mndass 12819) and has a two-sided neutral element (see mndid 12820), see also ismnd 12814. (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 12813*	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 12814*	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 12818), whose operation is associative (so, a semigroup, see also mndass 12819) and has a two-sided neutral element (see mndid 12820). (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 12815*	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 12816	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 12817	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 12818	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 12819	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 12820*	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 12821*	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 12822	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 12823	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 12824	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 12825	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 12826	The base set of a monoid is not empty. (It is also inhabited, as seen at mndidcl 12825). Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.)
|- B = ( Base ` G )   =>    |- ( G e. Mnd -> B =/= (/) )
Theorem	hashfinmndnn 12827	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 12828	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 12829	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 12830	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 12831	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 12832*	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 12833	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 12834	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 12835*	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 12836	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 12837*	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	ress0g 12838	0g is unaffected by restriction. This is a bit more generic than submnd0 12839. (Contributed by Thierry Arnoux, 23-Oct-2017.)
|- S = ( R ↾s A )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) -> .0. = ( 0g ` S ) )
Theorem	submnd0 12839	The zero of a submonoid is the same as the zero in the parent monoid. (Note that we must add the condition that the zero of the parent monoid is actually contained in the submonoid, because it is possible to have "subsets that are monoids" which are not submonoids because they have a different identity element. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- H = ( G ↾s S )   =>    |- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) -> .0. = ( 0g ` H ) )
Theorem	mndinvmod 12840*	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 12841	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 12842	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 12843	Hom-set generator class for monoids.
class MndHom
Syntax	csubmnd 12844	Class function taking a monoid to its lattice of submonoids.
class SubMnd
Definition	df-mhm 12845*	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 12846*	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 12847*	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 12848	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- ( F e. ( S MndHom T ) -> S e. Mnd )
Theorem	mhmrcl2 12849	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- ( F e. ( S MndHom T ) -> T e. Mnd )
Theorem	mhmf 12850	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 12851*	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 12852	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 12853	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 12854	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 12855	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 12856	Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- ( S e. (SubMnd ` M ) -> M e. Mnd )
Theorem	issubm 12857*	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 12858	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 12859*	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 12860	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 12861	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 12862	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 12863	Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- .0. = ( 0g ` M )   =>    |- ( S e. (SubMnd ` M ) -> .0. e. S )
Theorem	submcl 12864	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 12865	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 12866	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 ) )
Theorem	0mhm 12867	The constant zero linear function between two monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- .0. = ( 0g ` N )   &    |- B = ( Base ` M )   =>    |- ( ( M e. Mnd /\ N e. Mnd ) -> ( B X. { .0. } ) e. ( M MndHom N ) )
Theorem	mhmco 12868	The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( F o. G ) e. ( S MndHom U ) )
Theorem	mhmima 12869	The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- ( ( F e. ( M MndHom N ) /\ X e. (SubMnd ` M ) ) -> ( F " X ) e. (SubMnd ` N ) )
Theorem	mhmeql 12870	The equalizer of two monoid homomorphisms is a submonoid. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> dom ( F i^i G ) e. (SubMnd ` S ) )
7.2  Groups
7.2.1  Definition and basic properties
Syntax	cgrp 12871	Extend class notation with class of all groups.
class Grp
Syntax	cminusg 12872	Extend class notation with inverse of group element.
class invg
Syntax	csg 12873	Extend class notation with group subtraction (or division) operation.
class -g
Definition	df-grp 12874*	Define class of all groups. A group is a monoid (df-mnd 12812) whose internal operation is such that every element admits a left inverse (which can be proven to be a two-sided inverse). Thus, a group G is an algebraic structure formed from a base set of elements (notated ( Base ` G ) per df-base 12462) and an internal group operation (notated ( +g ` G ) per df-plusg 12543). The operation combines any two elements of the group base set and must satisfy the 4 group axioms: closure (the result of the group operation must always be a member of the base set, see grpcl 12879), associativity (so ( ( a +g b ) +g c ) = ( a +g ( b +g c ) ) for any a, b, c, see grpass 12880), identity (there must be an element e = ( 0g ` G ) such that e +g a = a +g e = a for any a), and inverse (for each element a in the base set, there must be an element b = invg a in the base set such that a +g b = b +g a = e). It can be proven that the identity element is unique (grpideu 12882). Groups need not be commutative; a commutative group is an Abelian group. Subgroups can often be formed from groups. An example of an (Abelian) group is the set of complex numbers CC over the group operation + (addition). Other structures include groups, including unital rings and fields. (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
Definition	df-minusg 12875*	Define inverse of group element. (Contributed by NM, 24-Aug-2011.)
|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
Definition	df-sbg 12876*	Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014.)
|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
Theorem	isgrp 12877*	The predicate "is a group". (This theorem demonstrates the use of symbols as variable names, first proposed by FL in 2010.) (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Grp <-> ( G e. Mnd /\ A. a e. B E. m e. B ( m .+ a ) = .0. ) )
Theorem	grpmnd 12878	A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. Grp -> G e. Mnd )
Theorem	grpcl 12879	Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
Theorem	grpass 12880	A group operation is associative. (Contributed by NM, 14-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
Theorem	grpinvex 12881*	Every member of a group has a left inverse. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> E. y e. B ( y .+ X ) = .0. )
Theorem	grpideu 12882*	The two-sided identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 8-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> E! u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) )
Theorem	grpmndd 12883	A group is a monoid. (Contributed by SN, 1-Jun-2024.)
|- ( ph -> G e. Grp )   =>    |- ( ph -> G e. Mnd )
Theorem	grpcld 12884	Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .+ Y ) e. B )
Theorem	grpplusf 12885	The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- F = ( +f ` G )   =>    |- ( G e. Grp -> F : ( B X. B ) --> B )
Theorem	grpplusfo 12886	The group addition operation is a function onto the base set/set of group elements. (Contributed by NM, 30-Oct-2006.) (Revised by AV, 30-Aug-2021.)
|- B = ( Base ` G )   &    |- F = ( +f ` G )   =>    |- ( G e. Grp -> F : ( B X. B ) -onto-> B )
Theorem	grppropd 12887*	If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Oct-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. Grp <-> L e. Grp ) )
Theorem	grpprop 12888	If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by NM, 11-Oct-2013.)
|- ( Base ` K ) = ( Base ` L )   &    |- ( +g ` K ) = ( +g ` L )   =>    |- ( K e. Grp <-> L e. Grp )
Theorem	grppropstrg 12889	Generalize a specific 2-element group L to show that any set K with the same (relevant) properties is also a group. (Contributed by NM, 28-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- ( Base ` K ) = B   &    |- ( +g ` K ) = .+   &    |- L = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }   =>    |- ( K e. V -> ( K e. Grp <-> L e. Grp ) )
Theorem	isgrpd2e 12890*	Deduce a group from its properties. In this version of isgrpd2 12891, we don't assume there is an expression for the inverse of x. (Contributed by NM, 10-Aug-2013.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> .0. = ( 0g ` G ) )   &    |- ( ph -> G e. Mnd )   &    |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = .0. )   =>    |- ( ph -> G e. Grp )
Theorem	isgrpd2 12891*	Deduce a group from its properties. N (negative) is normally dependent on x i.e. read it as N ( x ). Note: normally we don't use a ph antecedent on hypotheses that name structure components, since they can be eliminated with eqid 2177, but we make an exception for theorems such as isgrpd2 12891 and ismndd 12832 since theorems using them often rewrite the structure components. (Contributed by NM, 10-Aug-2013.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> .0. = ( 0g ` G ) )   &    |- ( ph -> G e. Mnd )   &    |- ( ( ph /\ x e. B ) -> N e. B )   &    |- ( ( ph /\ x e. B ) -> ( N .+ x ) = .0. )   =>    |- ( ph -> G e. Grp )
Theorem	isgrpde 12892*	Deduce a group from its properties. In this version of isgrpd 12893, we don't assume there is an expression for the inverse of x. (Contributed by NM, 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 ) -> E. y e. B ( y .+ x ) = .0. )   =>    |- ( ph -> G e. Grp )
Theorem	isgrpd 12893*	Deduce a group from its properties. Unlike isgrpd2 12891, this one goes straight from the base properties rather than going through Mnd. N (negative) is normally dependent on x i.e. read it as N ( x ). (Contributed by NM, 6-Jun-2013.) (Revised 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 ) -> N e. B )   &    |- ( ( ph /\ x e. B ) -> ( N .+ x ) = .0. )   =>    |- ( ph -> G e. Grp )
Theorem	isgrpi 12894*	Properties that determine a group. N (negative) is normally dependent on x i.e. read it as N ( x ). (Contributed by NM, 3-Sep-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ( x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- .0. e. B   &    |- ( x e. B -> ( .0. .+ x ) = x )   &    |- ( x e. B -> N e. B )   &    |- ( x e. B -> ( N .+ x ) = .0. )   =>    |- G e. Grp
Theorem	grpsgrp 12895	A group is a semigroup. (Contributed by AV, 28-Aug-2021.)
|- ( G e. Grp -> G e. Smgrp )
Theorem	dfgrp2 12896*	Alternate definition of a group as semigroup with a left identity and a left inverse for each element. This "definition" is weaker than df-grp 12874, based on the definition of a monoid which provides a left and a right identity. (Contributed by AV, 28-Aug-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Grp <-> ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) )
Theorem	dfgrp2e 12897*	Alternate definition of a group as a set with a closed, associative operation, a left identity and a left inverse for each element. Alternate definition in [Lang] p. 7. (Contributed by NM, 10-Oct-2006.) (Revised by AV, 28-Aug-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Grp <-> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) )
Theorem	grpidcl 12898	The identity element of a group belongs to the group. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> .0. e. B )
Theorem	grpbn0 12899	The base set of a group is not empty. It is also inhabited (see grpidcl 12898). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- B = ( Base ` G )   =>    |- ( G e. Grp -> B =/= (/) )
Theorem	grplid 12900	The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( .0. .+ X ) = X )