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	mulgfvalg 13901*	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 13902	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 13903	Existence of the group multiple operation. (Contributed by Jim Kingdon, 22-Apr-2025.)
|- ( G e. V -> (.g ` G ) e. _V )
Theorem	mulgfng 13904	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 13905	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 13906	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 13907*	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 13908*	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 13909	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 13910	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 13911	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 13912	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 13913	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 13914*	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 13915*	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 13916*	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 13917	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 13918	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 13919	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 13920	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 13921	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 13922	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 13923	Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 13918. (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 13924	Deduction associated with mulgcl 13919. (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 13925	Lemma for mulgaddcom 13926. (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 13926	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 13927	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 13928	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 ) )
Theorem	mulgnn0z 13929	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 13930	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 13931	Sum of group multiples, for positive multiples. (Contributed by Mario Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
Theorem	mulgnn0dir 13932	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 13933	Lemma for mulgdir 13934. (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 13934	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 13935	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 13936	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 13937	Product of group multiples, for positive multiples in a semigroup. (Contributed by Mario Carneiro, 13-Dec-2014.) (Revised by AV, 29-Aug-2021.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
Theorem	mulgnn0ass 13938	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 13939	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	mulgassr 13940	Reversed product of group multiples. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( N x. M ) .x. X ) = ( M .x. ( N .x. X ) ) )
Theorem	mulgmodid 13941	Casting out multiples of the identity element leaves the group multiple unchanged. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( ( N mod M ) .x. X ) = ( N .x. X ) )
Theorem	mulgsubdir 13942	Distribution of group multiples over subtraction for group elements, subdir 8703 analog. (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 13943	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	mulgpropdg 13944*	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.)
|- ( ph -> .x. = (.g ` G ) )   &    |- ( ph -> .X. = (.g ` H ) )   &    |- ( ph -> G e. V )   &    |- ( ph -> H e. W )   &    |- ( 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 13945	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 13946	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 ) )
7.2.3  Subgroups and Quotient groups
Syntax	csubg 13947	Extend class notation with all subgroups of a group.
class SubGrp
Syntax	cnsg 13948	Extend class notation with all normal subgroups of a group.
class NrmSGrp
Syntax	cqg 13949	Quotient group equivalence class.
class ~QG
Definition	df-subg 13950*	Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently (issubg2m 13969), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl 13964), contains the neutral element of the group (see subg0 13960) and contains the inverses for all of its elements (see subginvcl 13963). (Contributed by Mario Carneiro, 2-Dec-2014.)
|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
Definition	df-nsg 13951*	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 13952*	Define the equivalence relation in a group generated by a subgroup. More precisely, if G is a group and H is a subgroup, then G ~QG H is the equivalence relation on G associated with the left cosets of H. A typical application of this definition is the construction of the quotient group (resp. ring) of a group (resp. ring) by a normal subgroup (resp. two-sided ideal). (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 13953	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 13954	A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` G )   =>    |- ( S e. (SubGrp ` G ) -> S C_ B )
Theorem	subgid 13955	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	subgex 13956	The class of subgroups of a group is a set. (Contributed by Jim Kingdon, 8-Mar-2025.)
|- ( G e. Grp -> (SubGrp ` G ) e. _V )
Theorem	subggrp 13957	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 13958	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 13959	Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- ( S e. (SubGrp ` G ) -> G e. Grp )
Theorem	subg0 13960	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 13961	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 13962	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 13963	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 )
Theorem	subgcl 13964	A subgroup is closed under group operation. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- .+ = ( +g ` G )   =>    |- ( ( S e. (SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )
Theorem	subgsubcl 13965	A subgroup is closed under group subtraction. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- .- = ( -g ` G )   =>    |- ( ( S e. (SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .- Y ) e. S )
Theorem	subgsub 13966	The subtraction of elements in a subgroup is the same as subtraction in the group. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- .- = ( -g ` G )   &    |- H = ( G ↾s S )   &    |- N = ( -g ` H )   =>    |- ( ( S e. (SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .- Y ) = ( X N Y ) )
Theorem	subgmulgcl 13967	Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.)
|- .x. = (.g ` G )   =>    |- ( ( S e. (SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N .x. X ) e. S )
Theorem	subgmulg 13968	A group multiple is the same if evaluated in a subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.)
|- .x. = (.g ` G )   &    |- H = ( G ↾s S )   &    |- .xb = (.g ` H )   =>    |- ( ( S e. (SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N .x. X ) = ( N .xb X ) )
Theorem	issubg2m 13969*	Characterize the subgroups of a group by closure properties. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- I = ( invg ` G )   =>    |- ( G e. Grp -> ( S e. (SubGrp ` G ) <-> ( S C_ B /\ E. u u e. S /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) )
Theorem	issubgrpd2 13970*	Prove a subgroup by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014.)
|- ( ph -> S = ( I ↾s D ) )   &    |- ( ph -> .0. = ( 0g ` I ) )   &    |- ( ph -> .+ = ( +g ` I ) )   &    |- ( ph -> D C_ ( Base ` I ) )   &    |- ( ph -> .0. e. D )   &    |- ( ( ph /\ x e. D /\ y e. D ) -> ( x .+ y ) e. D )   &    |- ( ( ph /\ x e. D ) -> ( ( invg ` I ) ` x ) e. D )   &    |- ( ph -> I e. Grp )   =>    |- ( ph -> D e. (SubGrp ` I ) )
Theorem	issubgrpd 13971*	Prove a subgroup by closure. (Contributed by Stefan O'Rear, 7-Dec-2014.)
|- ( ph -> S = ( I ↾s D ) )   &    |- ( ph -> .0. = ( 0g ` I ) )   &    |- ( ph -> .+ = ( +g ` I ) )   &    |- ( ph -> D C_ ( Base ` I ) )   &    |- ( ph -> .0. e. D )   &    |- ( ( ph /\ x e. D /\ y e. D ) -> ( x .+ y ) e. D )   &    |- ( ( ph /\ x e. D ) -> ( ( invg ` I ) ` x ) e. D )   &    |- ( ph -> I e. Grp )   =>    |- ( ph -> S e. Grp )
Theorem	issubg3 13972*	A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- I = ( invg ` G )   =>    |- ( G e. Grp -> ( S e. (SubGrp ` G ) <-> ( S e. (SubMnd ` G ) /\ A. x e. S ( I ` x ) e. S ) ) )
Theorem	issubg4m 13973*	A subgroup is an inhabited subset of the group closed under subtraction. (Contributed by Mario Carneiro, 17-Sep-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   =>    |- ( G e. Grp -> ( S e. (SubGrp ` G ) <-> ( S C_ B /\ E. w w e. S /\ A. x e. S A. y e. S ( x .- y ) e. S ) ) )
Theorem	grpissubg 13974	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 (base set of the) group is subgroup of the other group. (Contributed by AV, 14-Mar-2019.)
|- B = ( Base ` G )   &    |- S = ( Base ` H )   =>    |- ( ( G e. Grp /\ H e. Grp ) -> ( ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> S e. (SubGrp ` G ) ) )
Theorem	resgrpisgrp 13975	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 other group restricted to the base set of the group is a group. (Contributed by AV, 14-Mar-2019.)
|- B = ( Base ` G )   &    |- S = ( Base ` H )   =>    |- ( ( G e. Grp /\ H e. Grp ) -> ( ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> ( G ↾s S ) e. Grp ) )
Theorem	subgsubm 13976	A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( S e. (SubGrp ` G ) -> S e. (SubMnd ` G ) )
Theorem	subsubg 13977	A subgroup of a subgroup is a subgroup. (Contributed by Mario Carneiro, 19-Jan-2015.)
|- H = ( G ↾s S )   =>    |- ( S e. (SubGrp ` G ) -> ( A e. (SubGrp ` H ) <-> ( A e. (SubGrp ` G ) /\ A C_ S ) ) )
Theorem	subgintm 13978*	The intersection of an inhabited collection of subgroups is a subgroup. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- ( ( S C_ (SubGrp ` G ) /\ E. w w e. S ) -> |^| S e. (SubGrp ` G ) )
Theorem	0subg 13979	The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014.) (Proof shortened by SN, 31-Jan-2025.)
|- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> { .0. } e. (SubGrp ` G ) )
Theorem	trivsubgd 13980	The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> B = { .0. } )   &    |- ( ph -> A e. (SubGrp ` G ) )   =>    |- ( ph -> A = B )
Theorem	trivsubgsnd 13981	The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> B = { .0. } )   =>    |- ( ph -> (SubGrp ` G ) = { B } )
Theorem	isnsg 13982*	Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( S e. (NrmSGrp ` G ) <-> ( S e. (SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) ) )
Theorem	isnsg2 13983*	Weaken the condition of isnsg 13982 to only one side of the implication. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( S e. (NrmSGrp ` G ) <-> ( S e. (SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S -> ( y .+ x ) e. S ) ) )
Theorem	nsgbi 13984	Defining property of a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( S e. (NrmSGrp ` G ) /\ A e. X /\ B e. X ) -> ( ( A .+ B ) e. S <-> ( B .+ A ) e. S ) )
Theorem	nsgsubg 13985	A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- ( S e. (NrmSGrp ` G ) -> S e. (SubGrp ` G ) )
Theorem	nsgconj 13986	The conjugation of an element of a normal subgroup is in the subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( S e. (NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> ( ( A .+ B ) .- A ) e. S )
Theorem	isnsg3 13987*	A subgroup is normal iff the conjugation of all the elements of the subgroup is in the subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( S e. (NrmSGrp ` G ) <-> ( S e. (SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) )
Theorem	elnmz 13988*	Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }   =>    |- ( A e. N <-> ( A e. X /\ A. z e. X ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) ) )
Theorem	nmzbi 13989*	Defining property of the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }   =>    |- ( ( A e. N /\ B e. X ) -> ( ( A .+ B ) e. S <-> ( B .+ A ) e. S ) )
Theorem	nmzsubg 13990*	The normalizer NG(S) of a subset S of the group is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Grp -> N e. (SubGrp ` G ) )
Theorem	ssnmz 13991*	A subgroup is a subset of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( S e. (SubGrp ` G ) -> S C_ N )
Theorem	isnsg4 13992*	A subgroup is normal iff its normalizer is the entire group. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( S e. (NrmSGrp ` G ) <-> ( S e. (SubGrp ` G ) /\ N = X ) )
Theorem	nmznsg 13993*	Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015.)
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- H = ( G ↾s N )   =>    |- ( S e. (SubGrp ` G ) -> S e. (NrmSGrp ` H ) )
Theorem	0nsg 13994	The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> { .0. } e. (NrmSGrp ` G ) )
Theorem	nsgid 13995	The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- B = ( Base ` G )   =>    |- ( G e. Grp -> B e. (NrmSGrp ` G ) )
Theorem	0idnsgd 13996	The whole group and the zero subgroup are normal subgroups of a group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Grp )   =>    |- ( ph -> { { .0. } , B } C_ (NrmSGrp ` G ) )
Theorem	trivnsgd 13997	The only normal subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> B = { .0. } )   =>    |- ( ph -> (NrmSGrp ` G ) = { B } )
Theorem	triv1nsgd 13998	A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> B = { .0. } )   =>    |- ( ph -> (NrmSGrp ` G ) ~~ 1o )
Theorem	1nsgtrivd 13999	A group with exactly one normal subgroup is trivial. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> (NrmSGrp ` G ) ~~ 1o )   =>    |- ( ph -> B = { .0. } )
Theorem	releqgg 14000	The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- R = ( G ~QG S )   =>    |- ( ( G e. V /\ S e. W ) -> Rel R )