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	grpidcl 13101	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 13102	The base set of a group is not empty. It is also inhabited (see grpidcl 13101). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- B = ( Base ` G )   =>    |- ( G e. Grp -> B =/= (/) )
Theorem	grplid 13103	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 13104	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 13105	The identity element of a group is a left identity. Deduction associated with grplid 13103. (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 13106	The identity element of a group is a right identity. Deduction associated with grprid 13104. (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 13107	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 13108	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 13109	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 13110*	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 13111	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 13112	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 13113*	Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 13095. (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 13114*	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 13115*	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 13116	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 13117*	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 13118	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 13119	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 13120	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 13121	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 13122	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 13123	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 13124	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 13125	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 13126*	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 13127	The left inverse of a group element. Deduction associated with grplinv 13122. (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 13128	The right inverse of a group element. Deduction associated with grprinv 13123. (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 13129*	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 13130*	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 13131*	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 13132	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 13133	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 12689. (Contributed by Jim Kingdon, 28-Feb-2025.)
|- B = ( Base ` G )   =>    |- ( G e. Grp -> ( G ↾s B ) e. Grp )
Theorem	grplcan 13134	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 13135	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 13136	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 13137	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 13138	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 13139	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 13140	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 13141	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 13142	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 13143	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 13144	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 13145	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 13146*	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	grpinvpropdg 13147*	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 -> K e. V )   &    |- ( ph -> L e. W )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( invg ` K ) = ( invg ` L ) )
Theorem	grpidssd 13148*	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 13149*	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 13150	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 13151	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 13152	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 13153	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 13154	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 13155	A df-neg 8193-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 13156	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 13157	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 )
Theorem	grpsubeq0 13158	If the difference between two group elements is zero, they are equal. (subeq0 8245 analog.) (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .- Y ) = .0. <-> X = Y ) )
Theorem	grpsubadd0sub 13159	Subtraction expressed as addition of the difference of the identity element and the subtrahend. (Contributed by AV, 9-Nov-2019.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .- = ( -g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( .0. .- Y ) ) )
Theorem	grpsubadd 13160	Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) = Z <-> ( Z .+ Y ) = X ) )
Theorem	grpsubsub 13161	Double group subtraction. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .- ( Y .- Z ) ) = ( X .+ ( Z .- Y ) ) )
Theorem	grpaddsubass 13162	Associative-type law for group subtraction and addition. (Contributed by NM, 16-Apr-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .- Z ) = ( X .+ ( Y .- Z ) ) )
Theorem	grppncan 13163	Cancellation law for subtraction (pncan 8225 analog). (Contributed by NM, 16-Apr-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) .- Y ) = X )
Theorem	grpnpcan 13164	Cancellation law for subtraction (npcan 8228 analog). (Contributed by NM, 19-Apr-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .- Y ) .+ Y ) = X )
Theorem	grpsubsub4 13165	Double group subtraction (subsub4 8252 analog). (Contributed by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) .- Z ) = ( X .- ( Z .+ Y ) ) )
Theorem	grppnpcan2 13166	Cancellation law for mixed addition and subtraction. (pnpcan2 8259 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Z ) .- ( Y .+ Z ) ) = ( X .- Y ) )
Theorem	grpnpncan 13167	Cancellation law for group subtraction. (npncan 8240 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) .+ ( Y .- Z ) ) = ( X .- Z ) )
Theorem	grpnpncan0 13168	Cancellation law for group subtraction (npncan2 8246 analog). (Contributed by AV, 24-Nov-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B ) ) -> ( ( X .- Y ) .+ ( Y .- X ) ) = .0. )
Theorem	grpnnncan2 13169	Cancellation law for group subtraction. (nnncan2 8256 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-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	dfgrp3mlem 13170*	Lemma for dfgrp3m 13171. (Contributed by AV, 28-Aug-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Smgrp /\ E. w w e. B /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) )
Theorem	dfgrp3m 13171*	Alternate definition of a group as semigroup (with at least one element) which is also a quasigroup, i.e. a magma in which solutions x and y of the equations ( a .+ x ) = b and ( x .+ a ) = b exist. Theorem 3.2 of [Bruck] p. 28. (Contributed by AV, 28-Aug-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Grp <-> ( G e. Smgrp /\ E. w w e. B /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) )
Theorem	dfgrp3me 13172*	Alternate definition of a group as a set with a closed, associative operation, for which solutions x and y of the equations ( a .+ x ) = b and ( x .+ a ) = b exist. Exercise 1 of [Herstein] p. 57. (Contributed by NM, 5-Dec-2006.) (Revised by AV, 28-Aug-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Grp <-> ( E. w w e. B /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) )
Theorem	grplactfval 13173*	The left group action of element A of group G. (Contributed by Paul Chapman, 18-Mar-2008.)
|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )   &    |- X = ( Base ` G )   =>    |- ( A e. X -> ( F ` A ) = ( a e. X |-> ( A .+ a ) ) )
Theorem	grplactcnv 13174*	The left group action of element A of group G maps the underlying set X of G one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- I = ( invg ` G )   =>    |- ( ( G e. Grp /\ A e. X ) -> ( ( F ` A ) : X -1-1-onto-> X /\ `' ( F ` A ) = ( F ` ( I ` A ) ) ) )
Theorem	grplactf1o 13175*	The left group action of element A of group G maps the underlying set X of G one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ A e. X ) -> ( F ` A ) : X -1-1-onto-> X )
Theorem	grpsubpropdg 13176	Weak property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 27-Mar-2015.)
|- ( ph -> ( Base ` G ) = ( Base ` H ) )   &    |- ( ph -> ( +g ` G ) = ( +g ` H ) )   &    |- ( ph -> G e. V )   &    |- ( ph -> H e. W )   =>    |- ( ph -> ( -g ` G ) = ( -g ` H ) )
Theorem	grpsubpropd2 13177*	Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> B = ( Base ` H ) )   &    |- ( ph -> G e. Grp )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )   =>    |- ( ph -> ( -g ` G ) = ( -g ` H ) )
Theorem	grp1 13178	The (smallest) structure representing a trivial group. According to Wikipedia ("Trivial group", 28-Apr-2019, https://en.wikipedia.org/wiki/Trivial_group) "In mathematics, a trivial group is a group consisting of a single element. All such groups are isomorphic, so one often speaks of the trivial group. The single element of the trivial group is the identity element". (Contributed by AV, 28-Apr-2019.)
|- M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }   =>    |- ( I e. V -> M e. Grp )
Theorem	grp1inv 13179	The inverse function of the trivial group. (Contributed by FL, 21-Jun-2010.) (Revised by AV, 26-Aug-2021.)
|- M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }   =>    |- ( I e. V -> ( invg ` M ) = ( _I |` { I } ) )
Theorem	imasgrp2 13180*	The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .+ = ( +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 ) -> N e. V )   &    |- ( ( ph /\ x e. V ) -> ( F ` ( N .+ x ) ) = ( F ` .0. ) )   =>    |- ( ph -> ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) )
Theorem	imasgrp 13181*	The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .+ = ( +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. Grp )   &    |- .0. = ( 0g ` R )   =>    |- ( ph -> ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) )
Theorem	imasgrpf1 13182	The image of a group under an injection is a group. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- U = ( F "s R )   &    |- V = ( Base ` R )   =>    |- ( ( F : V -1-1-> B /\ R e. Grp ) -> U e. Grp )
Theorem	qusgrp2 13183*	Prove that a quotient structure is a group. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .+ = ( +g ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. X )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .+ b ) .~ ( p .+ q ) ) )   &    |- ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )   &    |- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( x .+ y ) .+ z ) .~ ( x .+ ( y .+ z ) ) )   &    |- ( ph -> .0. e. V )   &    |- ( ( ph /\ x e. V ) -> ( .0. .+ x ) .~ x )   &    |- ( ( ph /\ x e. V ) -> N e. V )   &    |- ( ( ph /\ x e. V ) -> ( N .+ x ) .~ .0. )   =>    |- ( ph -> ( U e. Grp /\ [ .0. ] .~ = ( 0g ` U ) ) )
Theorem	mhmlem 13184*	Lemma for mhmmnd 13186 and ghmgrp 13188. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.)
|- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. X )   =>    |- ( ph -> ( F ` ( A .+ B ) ) = ( ( F ` A ) .+^ ( F ` B ) ) )
Theorem	mhmid 13185*	A surjective monoid morphism preserves identity element. (Contributed by Thierry Arnoux, 25-Jan-2020.)
|- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   &    |- X = ( Base ` G )   &    |- Y = ( Base ` H )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +g ` H )   &    |- ( ph -> F : X -onto-> Y )   &    |- ( ph -> G e. Mnd )   &    |- .0. = ( 0g ` G )   =>    |- ( ph -> ( F ` .0. ) = ( 0g ` H ) )
Theorem	mhmmnd 13186*	The image of a monoid G under a monoid homomorphism F is a monoid. (Contributed by Thierry Arnoux, 25-Jan-2020.)
|- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   &    |- X = ( Base ` G )   &    |- Y = ( Base ` H )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +g ` H )   &    |- ( ph -> F : X -onto-> Y )   &    |- ( ph -> G e. Mnd )   =>    |- ( ph -> H e. Mnd )
Theorem	mhmfmhm 13187*	The function fulfilling the conditions of mhmmnd 13186 is a monoid homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.)
|- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   &    |- X = ( Base ` G )   &    |- Y = ( Base ` H )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +g ` H )   &    |- ( ph -> F : X -onto-> Y )   &    |- ( ph -> G e. Mnd )   =>    |- ( ph -> F e. ( G MndHom H ) )
Theorem	ghmgrp 13188*	The image of a group G under a group homomorphism F is a group. This is a stronger result than that usually found in the literature, since the target of the homomorphism (operator O in our model) need not have any of the properties of a group as a prerequisite. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.)
|- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   &    |- X = ( Base ` G )   &    |- Y = ( Base ` H )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +g ` H )   &    |- ( ph -> F : X -onto-> Y )   &    |- ( ph -> G e. Grp )   =>    |- ( ph -> H e. Grp )
7.2.2  Group multiple operation The "group multiple" operation (if the group is multiplicative, also called "group power" or "group exponentiation" operation), can be defined for arbitrary magmas, if the multiplier/exponent is a nonnegative integer. See also the definition in [Lang] p. 6, where an element x(of a monoid) to the power of a nonnegative integer n is defined and denoted by x ^ n. Definition df-mulg 13190, however, defines the group multiple for arbitrary (i.e. also negative) integers. This is meaningful for groups only, and requires Definition df-minusg 13076 of the inverse operation invg.
Syntax	cmg 13189	Extend class notation with a function mapping a group operation to the multiple/power operation for the magma/group.
class .g
Definition	df-mulg 13190*	Define the group multiple function, also known as group exponentiation when viewed multiplicatively. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- .g = ( g e. _V |-> ( n e. ZZ , x e. ( Base ` g ) |-> if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) ) ) )
Theorem	mulgfvalg 13191*	Group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- I = ( invg ` G )   &    |- .x. = (.g ` G )   =>    |- ( G e. V -> .x. = ( n e. ZZ , x e. B |-> if ( n = 0 , .0. , if ( 0 < n , ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) )
Theorem	mulgval 13192	Value of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- I = ( invg ` G )   &    |- .x. = (.g ` G )   &    |- S = seq 1 ( .+ , ( NN X. { X } ) )   =>    |- ( ( N e. ZZ /\ X e. B ) -> ( N .x. X ) = if ( N = 0 , .0. , if ( 0 < N , ( S ` N ) , ( I ` ( S ` -u N ) ) ) ) )
Theorem	mulgex 13193	Existence of the group multiple operation. (Contributed by Jim Kingdon, 22-Apr-2025.)
|- ( G e. V -> (.g ` G ) e. _V )
Theorem	mulgfng 13194	Functionality of the group multiple operation. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( G e. V -> .x. Fn ( ZZ X. B ) )
Theorem	mulg0 13195	Group multiple (exponentiation) operation at zero. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .x. = (.g ` G )   =>    |- ( X e. B -> ( 0 .x. X ) = .0. )
Theorem	mulgnn 13196	Group multiple (exponentiation) operation at a positive integer. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .x. = (.g ` G )   &    |- S = seq 1 ( .+ , ( NN X. { X } ) )   =>    |- ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( S ` N ) )
Theorem	mulgnngsum 13197*	Group multiple (exponentiation) operation at a positive integer expressed by a group sum. (Contributed by AV, 28-Dec-2023.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- F = ( x e. ( 1 ... N ) |-> X )   =>    |- ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( G gsumg F ) )
Theorem	mulgnn0gsum 13198*	Group multiple (exponentiation) operation at a nonnegative integer expressed by a group sum. This corresponds to the definition in [Lang] p. 6, second formula. (Contributed by AV, 28-Dec-2023.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- F = ( x e. ( 1 ... N ) |-> X )   =>    |- ( ( N e. NN0 /\ X e. B ) -> ( N .x. X ) = ( G gsumg F ) )
Theorem	mulg1 13199	Group multiple (exponentiation) operation at one. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( X e. B -> ( 1 .x. X ) = X )
Theorem	mulgnnp1 13200	Group multiple (exponentiation) operation at a successor. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( N e. NN /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) )