P. 133 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13201-13300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pws0g 13201	The identity in a structure power of a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Mnd /\ I e. V ) -> ( I X. { .0. } ) = ( 0g ` Y ) )
Theorem	imasmnd2 13202*	The image structure of a monoid is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- ( 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 .+ b ) ) = ( F ` ( p .+ q ) ) ) )   &    |- ( ph -> R e. W )   &    |- ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )   &    |- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( ( x .+ y ) .+ z ) ) = ( F ` ( x .+ ( y .+ z ) ) ) )   &    |- ( ph -> .0. e. V )   &    |- ( ( ph /\ x e. V ) -> ( F ` ( .0. .+ x ) ) = ( F ` x ) )   &    |- ( ( ph /\ x e. V ) -> ( F ` ( x .+ .0. ) ) = ( F ` x ) )   =>    |- ( ph -> ( U e. Mnd /\ ( F ` .0. ) = ( 0g ` U ) ) )
Theorem	imasmnd 13203*	The image structure of a monoid is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- ( 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 .+ b ) ) = ( F ` ( p .+ q ) ) ) )   &    |- ( ph -> R e. Mnd )   &    |- .0. = ( 0g ` R )   =>    |- ( ph -> ( U e. Mnd /\ ( F ` .0. ) = ( 0g ` U ) ) )
Theorem	imasmndf1 13204	The image of a monoid under an injection is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- U = ( F "s R )   &    |- V = ( Base ` R )   =>    |- ( ( F : V -1-1-> B /\ R e. Mnd ) -> U e. Mnd )
Theorem	mnd1 13205	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 13206	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.6  Monoid homomorphisms and submonoids
Syntax	cmhm 13207	Hom-set generator class for monoids.
class MndHom
Syntax	csubmnd 13208	Class function taking a monoid to its lattice of submonoids.
class SubMnd
Definition	df-mhm 13209*	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 13210*	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 13211*	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	mhmex 13212	The set of monoid homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.)
|- ( ( S e. Mnd /\ T e. Mnd ) -> ( S MndHom T ) e. _V )
Theorem	mhmrcl1 13213	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- ( F e. ( S MndHom T ) -> S e. Mnd )
Theorem	mhmrcl2 13214	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- ( F e. ( S MndHom T ) -> T e. Mnd )
Theorem	mhmf 13215	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 13216*	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 13217	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 13218	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 13219	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 13220	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 13221	Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- ( S e. (SubMnd ` M ) -> M e. Mnd )
Theorem	issubm 13222*	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 13223	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 13224*	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 13225	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 13226	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 13227	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 13228	Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- .0. = ( 0g ` M )   =>    |- ( S e. (SubMnd ` M ) -> .0. e. S )
Theorem	submcl 13229	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	submmnd 13230	Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- H = ( M ↾s S )   =>    |- ( S e. (SubMnd ` M ) -> H e. Mnd )
Theorem	submbas 13231	The base set of a submonoid. (Contributed by Stefan O'Rear, 15-Jun-2015.)
|- H = ( M ↾s S )   =>    |- ( S e. (SubMnd ` M ) -> S = ( Base ` H ) )
Theorem	subm0 13232	Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- H = ( M ↾s S )   &    |- .0. = ( 0g ` M )   =>    |- ( S e. (SubMnd ` M ) -> .0. = ( 0g ` H ) )
Theorem	subsubm 13233	A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- H = ( G ↾s S )   =>    |- ( S e. (SubMnd ` G ) -> ( A e. (SubMnd ` H ) <-> ( A e. (SubMnd ` G ) /\ A C_ S ) ) )
Theorem	0subm 13234	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 13235	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 13236	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	resmhm 13237	Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
|- U = ( S ↾s X )   =>    |- ( ( F e. ( S MndHom T ) /\ X e. (SubMnd ` S ) ) -> ( F |` X ) e. ( U MndHom T ) )
Theorem	resmhm2 13238	One direction of resmhm2b 13239. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- U = ( T ↾s X )   =>    |- ( ( F e. ( S MndHom U ) /\ X e. (SubMnd ` T ) ) -> F e. ( S MndHom T ) )
Theorem	resmhm2b 13239	Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- U = ( T ↾s X )   =>    |- ( ( X e. (SubMnd ` T ) /\ ran F C_ X ) -> ( F e. ( S MndHom T ) <-> F e. ( S MndHom U ) ) )
Theorem	mhmco 13240	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 13241	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 13242	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.1.7  Iterated sums in a monoid One important use of words is as formal composites in cases where order is significant, using the general sum operator df-igsum 13009. If order is not significant, it is simpler to use families instead.
Theorem	gsumvallem2 13243*	Lemma for properties of the set of identities of G. The set of identities of a monoid is exactly the unique identity element. (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. Mnd -> O = { .0. } )
Theorem	gsumsubm 13244	Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> S e. (SubMnd ` G ) )   &    |- ( ph -> F : A --> S )   &    |- H = ( G ↾s S )   =>    |- ( ph -> ( G gsumg F ) = ( H gsumg F ) )
Theorem	gsumfzz 13245*	Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 15-Aug-2025.)
|- .0. = ( 0g ` G )   =>    |- ( ( G e. Mnd /\ M e. ZZ /\ N e. ZZ ) -> ( G gsumg ( k e. ( M ... N ) |-> .0. ) ) = .0. )
Theorem	gsumwsubmcl 13246	Closure of the composite in any submonoid. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.)
|- ( ( S e. (SubMnd ` G ) /\ W e. Word S ) -> ( G gsumg W ) e. S )
Theorem	gsumwcl 13247	Closure of the composite of a word in a structure G. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- B = ( Base ` G )   =>    |- ( ( G e. Mnd /\ W e. Word B ) -> ( G gsumg W ) e. B )
Theorem	gsumwmhm 13248	Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.)
|- B = ( Base ` M )   =>    |- ( ( H e. ( M MndHom N ) /\ W e. Word B ) -> ( H ` ( M gsumg W ) ) = ( N gsumg ( H o. W ) ) )
Theorem	gsumfzcl 13249	Closure of a finite group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 16-Aug-2025.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( G gsumg F ) e. B )
7.2  Groups
7.2.1  Definition and basic properties
Syntax	cgrp 13250	Extend class notation with class of all groups.
class Grp
Syntax	cminusg 13251	Extend class notation with inverse of group element.
class invg
Syntax	csg 13252	Extend class notation with group subtraction (or division) operation.
class -g
Definition	df-grp 13253*	Define class of all groups. A group is a monoid (df-mnd 13167) 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 12757) and an internal group operation (notated ( +g ` G ) per df-plusg 12841). 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 13258), associativity (so ( ( a +g b ) +g c ) = ( a +g ( b +g c ) ) for any a, b, c, see grpass 13259), 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 13261). 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 13254*	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 13255*	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 13256*	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 13257	A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. Grp -> G e. Mnd )
Theorem	grpcl 13258	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 13259	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 13260*	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 13261*	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	grpassd 13262	A group operation is associative. (Contributed by SN, 29-Jan-2025.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
Theorem	grpmndd 13263	A group is a monoid. (Contributed by SN, 1-Jun-2024.)
|- ( ph -> G e. Grp )   =>    |- ( ph -> G e. Mnd )
Theorem	grpcld 13264	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 13265	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 13266	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 13267*	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 13268	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 13269	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 13270*	Deduce a group from its properties. In this version of isgrpd2 13271, 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 13271*	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 2204, but we make an exception for theorems such as isgrpd2 13271 and ismndd 13187 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 13272*	Deduce a group from its properties. In this version of isgrpd 13273, 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 13273*	Deduce a group from its properties. Unlike isgrpd2 13271, 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 13274*	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 13275	A group is a semigroup. (Contributed by AV, 28-Aug-2021.)
|- ( G e. Grp -> G e. Smgrp )
Theorem	grpmgmd 13276	A group is a magma, deduction form. (Contributed by SN, 14-Apr-2025.)
|- ( ph -> G e. Grp )   =>    |- ( ph -> G e. Mgm )
Theorem	dfgrp2 13277*	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 13253, 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 13278*	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 13279	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 13280	The base set of a group is not empty. It is also inhabited (see grpidcl 13279). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- B = ( Base ` G )   =>    |- ( G e. Grp -> B =/= (/) )
Theorem	grplid 13281	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 )
Theorem	grprid 13282	The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( X .+ .0. ) = X )
Theorem	grplidd 13283	The identity element of a group is a left identity. Deduction associated with grplid 13281. (Contributed by SN, 29-Jan-2025.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( .0. .+ X ) = X )
Theorem	grpridd 13284	The identity element of a group is a right identity. Deduction associated with grprid 13282. (Contributed by SN, 29-Jan-2025.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( X .+ .0. ) = X )
Theorem	grpn0 13285	A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- ( G e. Grp -> G =/= (/) )
Theorem	hashfingrpnn 13286	A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> (♯ ` B ) e. NN )
Theorem	grprcan 13287	Right cancellation law for groups. (Contributed by NM, 24-Aug-2011.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Z ) = ( Y .+ Z ) <-> X = Y ) )
Theorem	grpinveu 13288*	The left inverse element of a group is unique. Lemma 2.2.1(b) of [Herstein] p. 55. (Contributed by NM, 24-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> E! y e. B ( y .+ X ) = .0. )
Theorem	grpid 13289	Two ways of saying that an element of a group is the identity element. Provides a convenient way to compute the value of the identity element. (Contributed by NM, 24-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( ( X .+ X ) = X <-> .0. = X ) )
Theorem	isgrpid2 13290	Properties showing that an element Z is the identity element of a group. (Contributed by NM, 7-Aug-2013.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> ( ( Z e. B /\ ( Z .+ Z ) = Z ) <-> .0. = Z ) )
Theorem	grpidd2 13291*	Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 13273. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> .0. e. B )   &    |- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )   &    |- ( ph -> G e. Grp )   =>    |- ( ph -> .0. = ( 0g ` G ) )
Theorem	grpinvfvalg 13292*	The inverse function of a group. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) (Revised by Rohan Ridenour, 13-Aug-2023.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( G e. V -> N = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) )
Theorem	grpinvval 13293*	The inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( X e. B -> ( N ` X ) = ( iota_ y e. B ( y .+ X ) = .0. ) )
Theorem	grpinvfng 13294	Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   =>    |- ( G e. V -> N Fn B )
Theorem	grpsubfvalg 13295*	Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-Feb-2024.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- I = ( invg ` G )   &    |- .- = ( -g ` G )   =>    |- ( G e. V -> .- = ( x e. B , y e. B |-> ( x .+ ( I ` y ) ) ) )
Theorem	grpsubval 13296	Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- I = ( invg ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( I ` Y ) ) )
Theorem	grpinvf 13297	The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   =>    |- ( G e. Grp -> N : B --> B )
Theorem	grpinvcl 13298	A group element's inverse is a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )
Theorem	grpinvcld 13299	A group element's inverse is a group element. (Contributed by SN, 29-Jan-2025.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( N ` X ) e. B )
Theorem	grplinv 13300	The left inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) .+ X ) = .0. )