P. 140 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13901-14000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	grpinvf 13901	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 13902	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 13903	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 13904	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 13905	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 13906	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 13907	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 13908*	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 13909	The left inverse of a group element. Deduction associated with grplinv 13904. (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 13910	The right inverse of a group element. Deduction associated with grprinv 13905. (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 13911*	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 13912*	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 13913*	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 13914	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 13915	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 13474. (Contributed by Jim Kingdon, 28-Feb-2025.)
|- B = ( Base ` G )   =>    |- ( G e. Grp -> ( G ↾s B ) e. Grp )
Theorem	grplcan 13916	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 13917	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 13918	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 13919	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 13920	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 13921	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 13922	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 13923	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 13924	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 13925	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 13926	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 13927	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 13928*	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 13929*	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 13930*	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 13931*	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 13932	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 13933	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 13934	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 13935	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 13936	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 13937	A df-neg 8501-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 13938	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 13939	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 13940	If the difference between two group elements is zero, they are equal. (subeq0 8553 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 13941	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 13942	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 13943	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 13944	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 13945	Cancellation law for subtraction (pncan 8533 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 13946	Cancellation law for subtraction (npcan 8536 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 13947	Double group subtraction (subsub4 8560 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 13948	Cancellation law for mixed addition and subtraction. (pnpcan2 8567 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 13949	Cancellation law for group subtraction. (npncan 8548 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 13950	Cancellation law for group subtraction (npncan2 8554 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 13951	Cancellation law for group subtraction. (nnncan2 8564 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 13952*	Lemma for dfgrp3m 13953. (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 13953*	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 13954*	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 13955*	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 13956*	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 13957*	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 13958	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 13959*	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 13960	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 13961	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 13962*	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 13963*	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 13964	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 13965*	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 13966*	Lemma for mhmmnd 13968 and ghmgrp 13970. (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 13967*	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 13968*	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 13969*	The function fulfilling the conditions of mhmmnd 13968 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 13970*	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 13972, however, defines the group multiple for arbitrary (i.e. also negative) integers. This is meaningful for groups only, and requires Definition df-minusg 13858 of the inverse operation invg.
Syntax	cmg 13971	Extend class notation with a function mapping a group operation to the multiple/power operation for the magma/group.
class .g
Definition	df-mulg 13972*	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 13973*	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 13974	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 13975	Existence of the group multiple operation. (Contributed by Jim Kingdon, 22-Apr-2025.)
|- ( G e. V -> (.g ` G ) e. _V )
Theorem	mulgfng 13976	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 13977	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 13978	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	mulgnngzsum 13979*	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 gzsumgz F ) )
Theorem	mulgnn0gzsum 13980*	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 gzsumgz F ) )
Theorem	mulg1 13981	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 13982	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 ) )
Theorem	mulg2 13983	Group multiple (exponentiation) operation at two. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( X e. B -> ( 2 .x. X ) = ( X .+ X ) )
Theorem	mulgnegnn 13984	Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- I = ( invg ` G )   =>    |- ( ( N e. NN /\ X e. B ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )
Theorem	mulgnn0p1 13985	Group multiple (exponentiation) operation at a successor, extended to NN0. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) )
Theorem	mulgnnsubcl 13986*	Closure of the group multiple (exponentiation) operation in a subsemigroup. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> S C_ B )   &    |- ( ( ph /\ x e. S /\ y e. S ) -> ( x .+ y ) e. S )   =>    |- ( ( ph /\ N e. NN /\ X e. S ) -> ( N .x. X ) e. S )
Theorem	mulgnn0subcl 13987*	Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> S C_ B )   &    |- ( ( ph /\ x e. S /\ y e. S ) -> ( x .+ y ) e. S )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> .0. e. S )   =>    |- ( ( ph /\ N e. NN0 /\ X e. S ) -> ( N .x. X ) e. S )
Theorem	mulgsubcl 13988*	Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> S C_ B )   &    |- ( ( ph /\ x e. S /\ y e. S ) -> ( x .+ y ) e. S )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> .0. e. S )   &    |- I = ( invg ` G )   &    |- ( ( ph /\ x e. S ) -> ( I ` x ) e. S )   =>    |- ( ( ph /\ N e. ZZ /\ X e. S ) -> ( N .x. X ) e. S )
Theorem	mulgnncl 13989	Closure of the group multiple (exponentiation) operation for a positive multiplier in a magma. (Contributed by Mario Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mgm /\ N e. NN /\ X e. B ) -> ( N .x. X ) e. B )
Theorem	mulgnn0cl 13990	Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N .x. X ) e. B )
Theorem	mulgcl 13991	Closure of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. X ) e. B )
Theorem	mulgneg 13992	Group multiple (exponentiation) operation at a negative integer. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- I = ( invg ` G )   =>    |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )
Theorem	mulgnegneg 13993	The inverse of a negative group multiple is the positive group multiple. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- I = ( invg ` G )   =>    |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( I ` ( -u N .x. X ) ) = ( N .x. X ) )
Theorem	mulgm1 13994	Group multiple (exponentiation) operation at negative one. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, 20-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- I = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( -u 1 .x. X ) = ( I ` X ) )
Theorem	mulgnn0cld 13995	Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 13990. (Contributed by SN, 1-Feb-2025.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( N .x. X ) e. B )
Theorem	mulgcld 13996	Deduction associated with mulgcl 13991. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( N .x. X ) e. B )
Theorem	mulgaddcomlem 13997	Lemma for mulgaddcom 13998. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( -u y .x. X ) .+ X ) = ( X .+ ( -u y .x. X ) ) )
Theorem	mulgaddcom 13998	The group multiple operator commutes with the group operation. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( ( N .x. X ) .+ X ) = ( X .+ ( N .x. X ) ) )
Theorem	mulginvcom 13999	The group multiple operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- I = ( invg ` G )   =>    |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. ( I ` X ) ) = ( I ` ( N .x. X ) ) )
Theorem	mulginvinv 14000	The group multiple operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- I = ( invg ` G )   =>    |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( I ` ( N .x. ( I ` X ) ) ) = ( N .x. X ) )