P. 132 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13101-13200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	idmhm 13101	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 13102	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 13103	Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- ( S e. (SubMnd ` M ) -> M e. Mnd )
Theorem	issubm 13104*	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 13105	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 13106*	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 13107	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 13108	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 13109	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 13110	Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- .0. = ( 0g ` M )   =>    |- ( S e. (SubMnd ` M ) -> .0. e. S )
Theorem	submcl 13111	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 13112	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 13113	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 13114	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 13115	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 13116	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 13117	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 13118	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 13119	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 13120	One direction of resmhm2b 13121. (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 13121	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 13122	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 13123	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 13124	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 12930. If order is not significant, it is simpler to use families instead.
Theorem	gsumvallem2 13125*	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 13126	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 13127*	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 13128	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 13129	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 13130	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 13131	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 13132	Extend class notation with class of all groups.
class Grp
Syntax	cminusg 13133	Extend class notation with inverse of group element.
class invg
Syntax	csg 13134	Extend class notation with group subtraction (or division) operation.
class -g
Definition	df-grp 13135*	Define class of all groups. A group is a monoid (df-mnd 13058) 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 12684) and an internal group operation (notated ( +g ` G ) per df-plusg 12768). 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 13140), associativity (so ( ( a +g b ) +g c ) = ( a +g ( b +g c ) ) for any a, b, c, see grpass 13141), 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 13143). 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 13136*	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 13137*	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 13138*	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 13139	A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. Grp -> G e. Mnd )
Theorem	grpcl 13140	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 13141	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 13142*	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 13143*	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 13144	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 13145	A group is a monoid. (Contributed by SN, 1-Jun-2024.)
|- ( ph -> G e. Grp )   =>    |- ( ph -> G e. Mnd )
Theorem	grpcld 13146	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 13147	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 13148	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 13149*	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 13150	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 13151	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 13152*	Deduce a group from its properties. In this version of isgrpd2 13153, 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 13153*	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 2196, but we make an exception for theorems such as isgrpd2 13153 and ismndd 13078 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 13154*	Deduce a group from its properties. In this version of isgrpd 13155, 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 13155*	Deduce a group from its properties. Unlike isgrpd2 13153, 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 13156*	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 13157	A group is a semigroup. (Contributed by AV, 28-Aug-2021.)
|- ( G e. Grp -> G e. Smgrp )
Theorem	grpmgmd 13158	A group is a magma, deduction form. (Contributed by SN, 14-Apr-2025.)
|- ( ph -> G e. Grp )   =>    |- ( ph -> G e. Mgm )
Theorem	dfgrp2 13159*	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 13135, 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 13160*	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 13161	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 13162	The base set of a group is not empty. It is also inhabited (see grpidcl 13161). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- B = ( Base ` G )   =>    |- ( G e. Grp -> B =/= (/) )
Theorem	grplid 13163	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 13164	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 13165	The identity element of a group is a left identity. Deduction associated with grplid 13163. (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 13166	The identity element of a group is a right identity. Deduction associated with grprid 13164. (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 13167	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 13168	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 13169	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 13170*	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 13171	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 13172	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 13173*	Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 13155. (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 13174*	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 13175*	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 13176	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 13177*	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 13178	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 13179	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 13180	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 13181	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 13182	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. )
Theorem	grprinv 13183	The right 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 ) -> ( X .+ ( N ` X ) ) = .0. )
Theorem	grpinvid1 13184	The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( N ` X ) = Y <-> ( X .+ Y ) = .0. ) )
Theorem	grpinvid2 13185	The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( N ` X ) = Y <-> ( Y .+ X ) = .0. ) )
Theorem	isgrpinv 13186*	Properties showing that a function M is the inverse function of a group. (Contributed by NM, 7-Aug-2013.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( G e. Grp -> ( ( M : B --> B /\ A. x e. B ( ( M ` x ) .+ x ) = .0. ) <-> N = M ) )
Theorem	grplinvd 13187	The left inverse of a group element. Deduction associated with grplinv 13182. (Contributed by SN, 29-Jan-2025.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( N ` X ) .+ X ) = .0. )
Theorem	grprinvd 13188	The right inverse of a group element. Deduction associated with grprinv 13183. (Contributed by SN, 29-Jan-2025.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( X .+ ( N ` X ) ) = .0. )
Theorem	grplrinv 13189*	In a group, every member has a left and right inverse. (Contributed by AV, 1-Sep-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> A. x e. B E. y e. B ( ( y .+ x ) = .0. /\ ( x .+ y ) = .0. ) )
Theorem	grpidinv2 13190*	A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010.) (Revised by AV, 1-Sep-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ A e. B ) -> ( ( ( .0. .+ A ) = A /\ ( A .+ .0. ) = A ) /\ E. y e. B ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) ) )
Theorem	grpidinv 13191*	A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006.) (Revised by AV, 1-Sep-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Grp -> E. u e. B A. x e. B ( ( ( u .+ x ) = x /\ ( x .+ u ) = x ) /\ E. y e. B ( ( y .+ x ) = u /\ ( x .+ y ) = u ) ) )
Theorem	grpinvid 13192	The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.)
|- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( G e. Grp -> ( N ` .0. ) = .0. )
Theorem	grpressid 13193	A group restricted to its base set is a group. It will usually be the original group exactly, of course, but to show that needs additional conditions such as those in strressid 12749. (Contributed by Jim Kingdon, 28-Feb-2025.)
|- B = ( Base ` G )   =>    |- ( G e. Grp -> ( G ↾s B ) e. Grp )
Theorem	grplcan 13194	Left cancellation law for groups. (Contributed by NM, 25-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Z .+ X ) = ( Z .+ Y ) <-> X = Y ) )
Theorem	grpasscan1 13195	An associative cancellation law for groups. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by AV, 30-Aug-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ ( ( N ` X ) .+ Y ) ) = Y )
Theorem	grpasscan2 13196	An associative cancellation law for groups. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .+ ( N ` Y ) ) .+ Y ) = X )
Theorem	grpidrcan 13197	If right adding an element of a group to an arbitrary element of the group results in this element, the added element is the identity element and vice versa. (Contributed by AV, 15-Mar-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( ( X .+ Z ) = X <-> Z = .0. ) )
Theorem	grpidlcan 13198	If left adding an element of a group to an arbitrary element of the group results in this element, the added element is the identity element and vice versa. (Contributed by AV, 15-Mar-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( ( Z .+ X ) = X <-> Z = .0. ) )
Theorem	grpinvinv 13199	Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( N ` ( N ` X ) ) = X )
Theorem	grpinvcnv 13200	The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   =>    |- ( G e. Grp -> `' N = N )