P. 175 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17401-17500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	frmdup1 17401*	Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- M = (freeMnd ` I )   &    |- B = ( Base ` G )   &    |- E = ( x e. Word I |-> ( G gsumg ( A o. x ) ) )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> I e. X )   &    |- ( ph -> A : I --> B )   =>    |- ( ph -> E e. ( M MndHom G ) )
Theorem	frmdup2 17402*	The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- M = (freeMnd ` I )   &    |- B = ( Base ` G )   &    |- E = ( x e. Word I |-> ( G gsumg ( A o. x ) ) )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> I e. X )   &    |- ( ph -> A : I --> B )   &    |- U = (varFMnd ` I )   &    |- ( ph -> Y e. I )   =>    |- ( ph -> ( E ` ( U ` Y ) ) = ( A ` Y ) )
Theorem	frmdup3lem 17403*	Lemma for frmdup3 17404. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- M = (freeMnd ` I )   &    |- B = ( Base ` G )   &    |- U = (varFMnd ` I )   =>    |- ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) -> F = ( x e. Word I |-> ( G gsumg ( A o. x ) ) ) )
Theorem	frmdup3 17404*	Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 18-Jul-2016.)
|- M = (freeMnd ` I )   &    |- B = ( Base ` G )   &    |- U = (varFMnd ` I )   =>    |- ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> E! m e. ( M MndHom G ) ( m o. U ) = A )
10.1.9  Examples and counterexamples for magmas, semigroups and monoids
Theorem	mgm2nsgrplem1 17405*	Lemma 1 for mgm2nsgrp 17409: M is a magma, even if A = B ( M is the trivial magma in this case, see mgmb1mgm1 17254). (Contributed by AV, 27-Jan-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )   =>    |- ( ( A e. V /\ B e. W ) -> M e. Mgm )
Theorem	mgm2nsgrplem2 17406*	Lemma 2 for mgm2nsgrp 17409. (Contributed by AV, 27-Jan-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )   &    |- .o. = ( +g ` M )   =>    |- ( ( A e. V /\ B e. W ) -> ( ( A .o. A ) .o. B ) = A )
Theorem	mgm2nsgrplem3 17407*	Lemma 3 for mgm2nsgrp 17409. (Contributed by AV, 28-Jan-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )   &    |- .o. = ( +g ` M )   =>    |- ( ( A e. V /\ B e. W ) -> ( A .o. ( A .o. B ) ) = B )
Theorem	mgm2nsgrplem4 17408*	Lemma 4 for mgm2nsgrp 17409: M is not a semigroup. (Contributed by AV, 28-Jan-2020.) (Proof shortened by AV, 31-Jan-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )   =>    |- ( ( # ` S ) = 2 -> M e/ SGrp )
Theorem	mgm2nsgrp 17409*	A small magma (with two elements) which is not a semigroup. (Contributed by AV, 28-Jan-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )   =>    |- ( ( # ` S ) = 2 -> ( M e. Mgm /\ M e/ SGrp ) )
Theorem	sgrp2nmndlem1 17410*	Lemma 1 for sgrp2nmnd 17417: M is a magma, even if A = B ( M is the trivial magma in this case, see mgmb1mgm1 17254). (Contributed by AV, 29-Jan-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )   =>    |- ( ( A e. V /\ B e. W ) -> M e. Mgm )
Theorem	sgrp2nmndlem2 17411*	Lemma 2 for sgrp2nmnd 17417. (Contributed by AV, 29-Jan-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )   &    |- .o. = ( +g ` M )   =>    |- ( ( A e. S /\ C e. S ) -> ( A .o. C ) = A )
Theorem	sgrp2nmndlem3 17412*	Lemma 3 for sgrp2nmnd 17417. (Contributed by AV, 29-Jan-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )   &    |- .o. = ( +g ` M )   =>    |- ( ( C e. S /\ B e. S /\ A =/= B ) -> ( B .o. C ) = B )
Theorem	sgrp2rid2 17413*	A small semigroup (with two elements) with two right identities which are different if A =/= B. (Contributed by AV, 10-Feb-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )   &    |- .o. = ( +g ` M )   =>    |- ( ( A e. V /\ B e. W ) -> A. x e. S A. y e. S ( y .o. x ) = y )
Theorem	sgrp2rid2ex 17414*	A small semigroup (with two elements) with two right identities which are different. (Contributed by AV, 10-Feb-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )   &    |- .o. = ( +g ` M )   =>    |- ( ( # ` S ) = 2 -> E. x e. S E. z e. S A. y e. S ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) )
Theorem	sgrp2nmndlem4 17415*	Lemma 4 for sgrp2nmnd 17417: M is a semigroup. (Contributed by AV, 29-Jan-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )   =>    |- ( ( # ` S ) = 2 -> M e. SGrp )
Theorem	sgrp2nmndlem5 17416*	Lemma 5 for sgrp2nmnd 17417: M is not a monoid. (Contributed by AV, 29-Jan-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )   =>    |- ( ( # ` S ) = 2 -> M e/ Mnd )
Theorem	sgrp2nmnd 17417*	A small semigroup (with two elements) which is not a monoid. (Contributed by AV, 26-Jan-2020.)
|- S = { A , B }   &    |- ( Base ` M ) = S   &    |- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )   =>    |- ( ( # ` S ) = 2 -> ( M e. SGrp /\ M e/ Mnd ) )
Theorem	mgmnsgrpex 17418	There is a magma which is not a semigroup. (Contributed by AV, 29-Jan-2020.)
|- E. m e. Mgm m e/ SGrp
Theorem	sgrpnmndex 17419	There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020.)
|- E. m e. SGrp m e/ Mnd
Theorem	sgrpssmgm 17420	The class of all semigroups is a proper subclass of the class of all magmas. (Contributed by AV, 29-Jan-2020.)
|- SGrp C. Mgm
Theorem	mndsssgrp 17421	The class of all monoids is a proper subclass of the class of all semigroups. (Contributed by AV, 29-Jan-2020.)
|- Mnd C. SGrp
10.2  Groups
10.2.1  Definition and basic properties
Syntax	cgrp 17422	Extend class notation with class of all groups.
class Grp
Syntax	cminusg 17423	Extend class notation with inverse of group element.
class invg
Syntax	csg 17424	Extend class notation with group subtraction (or division) operation.
class -g
Definition	df-grp 17425*	Define class of all groups. A group is a monoid (df-mnd 17295) 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 15863) and an internal group operation (notated ( +g ` G ) per df-plusg 15954). 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 17430), associativity (so ( ( a +g b ) +g c ) = ( a +g ( b +g c ) ) for any a, b, c, see grpass 17431), 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 17433). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 18196). Subgroups can often be formed from groups, see df-subg 17591. An example of an (Abelian) group is the set of complex numbers CC over the group operation + (addition), as proven in cnaddablx 18271; an Abelian group is a group as proven in ablgrp 18198. Other structures include groups, including unital rings (df-ring 18549) and fields (df-field 18750). (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 17426*	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 17427*	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 17428*	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 17429	A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. Grp -> G e. Mnd )
Theorem	grpcl 17430	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 17431	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 17432*	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 17433*	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	grpplusf 17434	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 17435	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	resgrpplusfrn 17436	The underlying set of a group operation which is a restriction of a structure. (Contributed by Paul Chapman, 25-Mar-2008.) (Revised by AV, 30-Aug-2021.)
|- B = ( Base ` G )   &    |- H = ( G ↾s S )   &    |- F = ( +f ` H )   =>    |- ( ( H e. Grp /\ S C_ B ) -> S = ran F )
Theorem	grppropd 17437*	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 17438	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	grppropstr 17439	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. Grp <-> L e. Grp )
Theorem	grpss 17440	Show that a structure extending a constructed group (e.g., a ring) is also a group. This allows us to prove that a constructed potential ring R is a group before we know that it is also a ring. (Theorem ringgrp 18552, on the other hand, requires that we know in advance that R is a ring.) (Contributed by NM, 11-Oct-2013.)
|- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }   &    |- R e. _V   &    |- G C_ R   &    |- Fun R   =>    |- ( G e. Grp <-> R e. Grp )
Theorem	isgrpd2e 17441*	Deduce a group from its properties. In this version of isgrpd2 17442, 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 17442*	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 2622, but we make an exception for theorems such as isgrpd2 17442, ismndd 17313, and islmodd 18869 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 17443*	Deduce a group from its properties. In this version of isgrpd 17444, 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 17444*	Deduce a group from its properties. Unlike isgrpd2 17442, 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 17445*	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 17446	A group is a semigroup. (Contributed by AV, 28-Aug-2021.)
|- ( G e. Grp -> G e. SGrp )
Theorem	dfgrp2 17447*	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 17425, 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. SGrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) )
Theorem	dfgrp2e 17448*	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	isgrpix 17449*	Properties that determine a group. Read N as N ( x ). Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.)
|- B e. _V   &    |- .+ e. _V   &    |- G = { <. 1 , B >. , <. 2 , .+ >. }   &    |- ( ( 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	grpidcl 17450	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 17451	The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- B = ( Base ` G )   =>    |- ( G e. Grp -> B =/= (/) )
Theorem	grplid 17452	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 17453	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	grpn0 17454	A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- ( G e. Grp -> G =/= (/) )
Theorem	grprcan 17455	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 17456*	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 17457	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 17458	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 17459*	Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 17444. (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	grpinvfval 17460*	The inverse function of a group. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- N = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) )
Theorem	grpinvval 17461*	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	grpinvfn 17462	Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   =>    |- N Fn B
Theorem	grpinvfvi 17463	The group inverse function is compatible with identity-function protection. (Contributed by Stefan O'Rear, 21-Mar-2015.)
|- N = ( invg ` G )   =>    |- N = ( invg ` ( _I ` G ) )
Theorem	grpsubfval 17464*	Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- I = ( invg ` G )   &    |- .- = ( -g ` G )   =>    |- .- = ( x e. B , y e. B |-> ( x .+ ( I ` y ) ) )
Theorem	grpsubval 17465	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 17466	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 17467	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	grplinv 17468	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 17469	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 17470	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 17471	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 17472*	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	grplrinv 17473*	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 17474*	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 17475*	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 17476	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	grplcan 17477	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 17478	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 17479	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 17480	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 17481	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 17482	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 17483	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 )
Theorem	grpinv11 17484	The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) = ( N ` Y ) <-> X = Y ) )
Theorem	grpinvf1o 17485	The group inverse is a one-to-one onto function. (Contributed by NM, 22-Oct-2014.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   &    |- ( ph -> G e. Grp )   =>    |- ( ph -> N : B -1-1-onto-> B )
Theorem	grpinvnz 17486	The inverse of a nonzero group element is not zero. (Contributed by Stefan O'Rear, 27-Feb-2015.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ X =/= .0. ) -> ( N ` X ) =/= .0. )
Theorem	grpinvnzcl 17487	The inverse of a nonzero group element is a nonzero group element. (Contributed by Stefan O'Rear, 27-Feb-2015.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. ( B \ { .0. } ) ) -> ( N ` X ) e. ( B \ { .0. } ) )
Theorem	grpsubinv 17488	Subtraction of an inverse. (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- N = ( invg ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .- ( N ` Y ) ) = ( X .+ Y ) )
Theorem	grplmulf1o 17489*	Left multiplication by a group element is a bijection on any group. (Contributed by Mario Carneiro, 17-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- F = ( x e. B |-> ( X .+ x ) )   =>    |- ( ( G e. Grp /\ X e. B ) -> F : B -1-1-onto-> B )
Theorem	grpinvpropd 17490*	If two structures have the same group components (properties), they have the same group inversion function. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Stefan O'Rear, 21-Mar-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 -> ( invg ` K ) = ( invg ` L ) )
Theorem	grpidssd 17491*	If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then both groups have the same identity element. (Contributed by AV, 15-Mar-2019.)
|- ( ph -> M e. Grp )   &    |- ( ph -> S e. Grp )   &    |- B = ( Base ` S )   &    |- ( ph -> B C_ ( Base ` M ) )   &    |- ( ph -> A. x e. B A. y e. B ( x ( +g ` M ) y ) = ( x ( +g ` S ) y ) )   =>    |- ( ph -> ( 0g ` M ) = ( 0g ` S ) )
Theorem	grpinvssd 17492*	If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then the elements of the first group have the same inverses in both groups. (Contributed by AV, 15-Mar-2019.)
|- ( ph -> M e. Grp )   &    |- ( ph -> S e. Grp )   &    |- B = ( Base ` S )   &    |- ( ph -> B C_ ( Base ` M ) )   &    |- ( ph -> A. x e. B A. y e. B ( x ( +g ` M ) y ) = ( x ( +g ` S ) y ) )   =>    |- ( ph -> ( X e. B -> ( ( invg ` S ) ` X ) = ( ( invg ` M ) ` X ) ) )
Theorem	grpinvadd 17493	The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( N ` ( X .+ Y ) ) = ( ( N ` Y ) .+ ( N ` X ) ) )
Theorem	grpsubf 17494	Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   =>    |- ( G e. Grp -> .- : ( B X. B ) --> B )
Theorem	grpsubcl 17495	Closure of group subtraction. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .- Y ) e. B )
Theorem	grpsubrcan 17496	Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Z ) = ( Y .- Z ) <-> X = Y ) )
Theorem	grpinvsub 17497	Inverse of a group subtraction. (Contributed by NM, 9-Sep-2014.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( N ` ( X .- Y ) ) = ( Y .- X ) )
Theorem	grpinvval2 17498	A df-neg 10269-like equation for inverse in terms of group subtraction. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- N = ( invg ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) = ( .0. .- X ) )
Theorem	grpsubid 17499	Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( X .- X ) = .0. )
Theorem	grpsubid1 17500	Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( X .- .0. ) = X )