P. 160 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15901-16000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	grpinvinv 15901	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 15902	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 15903	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 15904	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 15905	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 15906	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 15907	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 15908*	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 15909*	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 15910*	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 15911*	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 15912	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 15913	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 15914	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 15915	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 15916	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 15917	A df-neg 9799-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 15918	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 15919	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 15920	If the difference between two group elements is zero, they are equal. (subeq0 9836 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 15921	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 15922	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 15923	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 15924	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 15925	Cancellation law for subtraction (pncan 9817 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 15926	Cancellation law for subtraction (npcan 9820 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 15927	Double group subtraction (subsub4 9843 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 15928	Cancellation law for mixed addition and subtraction. (pnpcan2 9850 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 15929	Cancellation law for group subtraction. (npncan 9831 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 15930	Cancellation law for group subtraction (npncan2 9837 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 15931	Cancellation law for group subtraction. (nnncan2 9847 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	grplactfval 15932*	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	grplactval 15933*	The value of the left group action of element A of group G at B. (Contributed by Paul Chapman, 18-Mar-2008.)
|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )   &    |- X = ( Base ` G )   =>    |- ( ( A e. X /\ B e. X ) -> ( ( F ` A ) ` B ) = ( A .+ B ) )
Theorem	grplactcnv 15934*	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 15935*	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	grpsubpropd 15936	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 ` G ) = ( -g ` H ) )
Theorem	grpsubpropd2 15937*	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	mulgfval 15938*	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 )   =>    |- .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 15939	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	mulgfn 15940	Functionality of the group multiple function. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- .x. Fn ( ZZ X. B )
Theorem	mulgfvi 15941	The group multiple function is compatible with identity-function protection. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- .x. = (.g ` G )   =>    |- .x. = (.g ` ( _I ` G ) )
Theorem	mulg0 15942	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 15943	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	mulg1 15944	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 15945	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 15946	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 15947	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 15948	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 15949*	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 15950*	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 15951*	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 15952	Closure of the group multiple (exponentiation) operation. TODO: This can be generalized to a magma if/when we introduce them. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mnd /\ N e. NN /\ X e. B ) -> ( N .x. X ) e. B )
Theorem	mulgnn0cl 15953	Closure of the group multiple (exponentiation) operation. (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 15954	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 15955	Group multiple (exponentiation) operation at a negative integer. (Contributed 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	mulgm1 15956	Group multiple (exponentiation) operation at negative one. (Contributed 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	mulgnn0z 15957	A group multiple of the identity, for nonnegative multiple. (Contributed by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Mnd /\ N e. NN0 ) -> ( N .x. .0. ) = .0. )
Theorem	mulgz 15958	A group multiple of the identity, for integer multiple. (Contributed by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ N e. ZZ ) -> ( N .x. .0. ) = .0. )
Theorem	mulgnndir 15959	Sum of group multiples, for positive multiples. TODO: This can be generalized to a semigroup if/when we introduce them. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
Theorem	mulgnn0dir 15960	Sum of group multiples, generalized to NN0. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
Theorem	mulgdirlem 15961	Lemma for mulgdir 15962. (Contributed by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
Theorem	mulgdir 15962	Sum of group multiples, generalized to ZZ. (Contributed by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
Theorem	mulgp1 15963	Group multiple (exponentiation) operation at a successor, extended to ZZ. (Contributed by Mario Carneiro, 11-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) )
Theorem	mulgneg2 15964	Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- I = ( invg ` G )   =>    |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( -u N .x. X ) = ( N .x. ( I ` X ) ) )
Theorem	mulgnnass 15965	Product of group multiples, for positive multiples. TODO: This can be generalized to a semigroup if/when we introduce them. (Contributed by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mnd /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
Theorem	mulgnn0ass 15966	Product of group multiples, generalized to NN0. (Contributed by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
Theorem	mulgass 15967	Product of group multiples, generalized to ZZ. (Contributed by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
Theorem	mulgsubdir 15968	Subtraction of a group element from itself. (Contributed by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M - N ) .x. X ) = ( ( M .x. X ) .- ( N .x. X ) ) )
Theorem	mhmmulg 15969	A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .X. = (.g ` H )   =>    |- ( ( F e. ( G MndHom H ) /\ N e. NN0 /\ X e. B ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )
Theorem	mulgpropd 15970*	Two structures with the same group-nature have the same group multiple function. K is expected to either be _V (when strong equality is available) or B (when closure is available). (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- .x. = (.g ` G )   &    |- .X. = (.g ` H )   &    |- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> B = ( Base ` H ) )   &    |- ( ph -> B C_ K )   &    |- ( ( ph /\ ( x e. K /\ y e. K ) ) -> ( x ( +g ` G ) y ) e. K )   &    |- ( ( ph /\ ( x e. K /\ y e. K ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )   =>    |- ( ph -> .x. = .X. )
Theorem	submmulgcl 15971	Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 13-Jan-2015.)
|- .xb = (.g ` G )   =>    |- ( ( S e. (SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> ( N .xb X ) e. S )
Theorem	submmulg 15972	A group multiple is the same if evaluated in a submonoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- .xb = (.g ` G )   &    |- H = ( G ↾s S )   &    |- .x. = (.g ` H )   =>    |- ( ( S e. (SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> ( N .xb X ) = ( N .x. X ) )
Theorem	prdsinvlem 15973*	Characterization of inverses in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R : I --> Grp )   &    |- ( ph -> F e. B )   &    |- .0. = ( 0g o. R )   &    |- N = ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( F ` y ) ) )   =>    |- ( ph -> ( N e. B /\ ( N .+ F ) = .0. ) )
Theorem	prdsgrpd 15974	The product of a family of groups is a group. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Grp )   =>    |- ( ph -> Y e. Grp )
Theorem	prdsinvgd 15975*	Negation in a product of groups. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Grp )   &    |- B = ( Base ` Y )   &    |- N = ( invg ` Y )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( N ` X ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) )
Theorem	pwsgrp 15976	The product of a family of groups is a group. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. Grp /\ I e. V ) -> Y e. Grp )
Theorem	pwsinvg 15977	Negation in a group power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- M = ( invg ` R )   &    |- N = ( invg ` Y )   =>    |- ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( N ` X ) = ( M o. X ) )
Theorem	pwssub 15978	Subtraction in a group power. (Contributed by Mario Carneiro, 12-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- M = ( -g ` R )   &    |- .- = ( -g ` Y )   =>    |- ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F .- G ) = ( F oF M G ) )
Theorem	pwsmulg 15979	Value of a group multiple in a structure power. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- .xb = (.g ` Y )   &    |- .x. = (.g ` R )   =>    |- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( ( N .xb X ) ` A ) = ( N .x. ( X ` A ) ) )
Theorem	imasgrp2 15980*	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 15981*	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 15982	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	divsgrp2 15983*	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	xpsgrp 15984	The binary product of groups is a group. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- T = ( R X.s S )   =>    |- ( ( R e. Grp /\ S e. Grp ) -> T e. Grp )
10.2.2  Subgroups and Quotient groups
Syntax	csubg 15985	Extend class notation with all subgroups of a group.
class SubGrp
Syntax	cnsg 15986	Extend class notation with all normal subgroups of a group.
class NrmSGrp
Syntax	cqg 15987	Quotient group equivalence class.
class ~QG
Definition	df-subg 15988*	Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently (issubg2 16006), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl 16001), contains the neutral element of the group (see subg0 15997) and contains the inverses for all of its elements (see subginvcl 16000). (Contributed by Mario Carneiro, 2-Dec-2014.)
|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
Definition	df-nsg 15989*	Define the equivalence relation in a quotient ring or quotient group (where i is a two-sided ideal or a normal subgroup). For non-normal subgroups this generates the left cosets. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- NrmSGrp = ( w e. Grp |-> { s e. (SubGrp ` w ) | [. ( Base ` w ) / b ]. [. ( +g ` w ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) } )
Definition	df-eqg 15990*	Define the equivalence relation in a quotient ring or quotient group (where i is a two-sided ideal or a normal subgroup). For non-normal subgroups this generates the left cosets. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
Theorem	issubg 15991	The subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` G )   =>    |- ( S e. (SubGrp ` G ) <-> ( G e. Grp /\ S C_ B /\ ( G ↾s S ) e. Grp ) )
Theorem	subgss 15992	A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` G )   =>    |- ( S e. (SubGrp ` G ) -> S C_ B )
Theorem	subgid 15993	A group is a subgroup of itself. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- B = ( Base ` G )   =>    |- ( G e. Grp -> B e. (SubGrp ` G ) )
Theorem	subggrp 15994	A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- H = ( G ↾s S )   =>    |- ( S e. (SubGrp ` G ) -> H e. Grp )
Theorem	subgbas 15995	The base of the restricted group in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- H = ( G ↾s S )   =>    |- ( S e. (SubGrp ` G ) -> S = ( Base ` H ) )
Theorem	subgrcl 15996	Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- ( S e. (SubGrp ` G ) -> G e. Grp )
Theorem	subg0 15997	A subgroup of a group must have the same identity as the group. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- H = ( G ↾s S )   &    |- .0. = ( 0g ` G )   =>    |- ( S e. (SubGrp ` G ) -> .0. = ( 0g ` H ) )
Theorem	subginv 15998	The inverse of an element in a subgroup is the same as the inverse in the larger group. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- H = ( G ↾s S )   &    |- I = ( invg ` G )   &    |- J = ( invg ` H )   =>    |- ( ( S e. (SubGrp ` G ) /\ X e. S ) -> ( I ` X ) = ( J ` X ) )
Theorem	subg0cl 15999	The group identity is an element of any subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- .0. = ( 0g ` G )   =>    |- ( S e. (SubGrp ` G ) -> .0. e. S )
Theorem	subginvcl 16000	The inverse of an element is closed in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- I = ( invg ` G )   =>    |- ( ( S e. (SubGrp ` G ) /\ X e. S ) -> ( I ` X ) e. S )