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	mulginvinv 13901	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 13902	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 13903	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 13904	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 13905	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 13906	Lemma for mulgdir 13907. (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 13907	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 13908	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 13909	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 13910	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 13911	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 13912	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 13913	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 13914	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 13915	Distribution of group multiples over subtraction for group elements, subdir 8676 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 13916	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 13917*	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 13918	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 13919	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 13920	Extend class notation with all subgroups of a group.
class SubGrp
Syntax	cnsg 13921	Extend class notation with all normal subgroups of a group.
class NrmSGrp
Syntax	cqg 13922	Quotient group equivalence class.
class ~QG
Definition	df-subg 13923*	Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently (issubg2m 13942), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl 13937), contains the neutral element of the group (see subg0 13933) and contains the inverses for all of its elements (see subginvcl 13936). (Contributed by Mario Carneiro, 2-Dec-2014.)
|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
Definition	df-nsg 13924*	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 13925*	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 13926	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 13927	A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` G )   =>    |- ( S e. (SubGrp ` G ) -> S C_ B )
Theorem	subgid 13928	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 13929	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 13930	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 13931	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 13932	Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- ( S e. (SubGrp ` G ) -> G e. Grp )
Theorem	subg0 13933	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 13934	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 13935	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 13936	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 13937	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 13938	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 13939	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 13940	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 13941	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 13942*	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 13943*	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 13944*	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 13945*	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 13946*	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 13947	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 13948	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 13949	A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( S e. (SubGrp ` G ) -> S e. (SubMnd ` G ) )
Theorem	subsubg 13950	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 13951*	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 13952	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 13953	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 13954	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 13955*	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 13956*	Weaken the condition of isnsg 13955 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 13957	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 13958	A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- ( S e. (NrmSGrp ` G ) -> S e. (SubGrp ` G ) )
Theorem	nsgconj 13959	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 13960*	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 13961*	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 13962*	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 13963*	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 13964*	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 13965*	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 13966*	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 13967	The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> { .0. } e. (NrmSGrp ` G ) )
Theorem	nsgid 13968	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 13969	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 13970	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 13971	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 13972	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 13973	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 )
Theorem	eqgex 13974	The left coset equivalence relation exists. (Contributed by Jim Kingdon, 25-Apr-2025.)
|- ( ( G e. V /\ S e. W ) -> ( G ~QG S ) e. _V )
Theorem	eqgfval 13975*	Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.)
|- X = ( Base ` G )   &    |- N = ( invg ` G )   &    |- .+ = ( +g ` G )   &    |- R = ( G ~QG S )   =>    |- ( ( G e. V /\ S C_ X ) -> R = { <. x , y >. | ( { x , y } C_ X /\ ( ( N ` x ) .+ y ) e. S ) } )
Theorem	eqgval 13976	Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.) (Revised by Mario Carneiro, 14-Jun-2015.)
|- X = ( Base ` G )   &    |- N = ( invg ` G )   &    |- .+ = ( +g ` G )   &    |- R = ( G ~QG S )   =>    |- ( ( G e. V /\ S C_ X ) -> ( A R B <-> ( A e. X /\ B e. X /\ ( ( N ` A ) .+ B ) e. S ) ) )
Theorem	eqger 13977	The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- .~ = ( G ~QG Y )   =>    |- ( Y e. (SubGrp ` G ) -> .~ Er X )
Theorem	eqglact 13978*	A left coset can be expressed as the image of a left action. (Contributed by Mario Carneiro, 20-Sep-2015.)
|- X = ( Base ` G )   &    |- .~ = ( G ~QG Y )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ Y C_ X /\ A e. X ) -> [ A ] .~ = ( ( x e. X |-> ( A .+ x ) ) " Y ) )
Theorem	eqgid 13979	The left coset containing the identity is the original subgroup. (Contributed by Mario Carneiro, 20-Sep-2015.)
|- X = ( Base ` G )   &    |- .~ = ( G ~QG Y )   &    |- .0. = ( 0g ` G )   =>    |- ( Y e. (SubGrp ` G ) -> [ .0. ] .~ = Y )
Theorem	eqgen 13980	Each coset is equipotent to the subgroup itself (which is also the coset containing the identity). (Contributed by Mario Carneiro, 20-Sep-2015.)
|- X = ( Base ` G )   &    |- .~ = ( G ~QG Y )   =>    |- ( ( Y e. (SubGrp ` G ) /\ A e. ( X /. .~ ) ) -> Y ~~ A )
Theorem	eqgcpbl 13981	The subgroup coset equivalence relation is compatible with addition when the subgroup is normal. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- X = ( Base ` G )   &    |- .~ = ( G ~QG Y )   &    |- .+ = ( +g ` G )   =>    |- ( Y e. (NrmSGrp ` G ) -> ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) ) )
Theorem	eqg0el 13982	Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.)
|- .~ = ( G ~QG H )   =>    |- ( ( G e. Grp /\ H e. (SubGrp ` G ) ) -> ( [ X ] .~ = H <-> X e. H ) )
Theorem	quselbasg 13983*	Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.)
|- .~ = ( G ~QG S )   &    |- U = ( G /.s .~ )   &    |- B = ( Base ` G )   =>    |- ( ( G e. V /\ X e. W /\ S e. Z ) -> ( X e. ( Base ` U ) <-> E. x e. B X = [ x ] .~ ) )
Theorem	quseccl0g 13984	Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) Generalization of quseccl 13986 for arbitrary sets G. (Revised by AV, 24-Feb-2025.)
|- .~ = ( G ~QG S )   &    |- H = ( G /.s .~ )   &    |- C = ( Base ` G )   &    |- B = ( Base ` H )   =>    |- ( ( G e. V /\ X e. C /\ S e. Z ) -> [ X ] .~ e. B )
Theorem	qusgrp 13985	If Y is a normal subgroup of G, then H = G / Y is a group, called the quotient of G by Y. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- H = ( G /.s ( G ~QG S ) )   =>    |- ( S e. (NrmSGrp ` G ) -> H e. Grp )
Theorem	quseccl 13986	Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) (Proof shortened by AV, 9-Mar-2025.)
|- H = ( G /.s ( G ~QG S ) )   &    |- V = ( Base ` G )   &    |- B = ( Base ` H )   =>    |- ( ( S e. (NrmSGrp ` G ) /\ X e. V ) -> [ X ] ( G ~QG S ) e. B )
Theorem	qusadd 13987	Value of the group operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.)
|- H = ( G /.s ( G ~QG S ) )   &    |- V = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+b = ( +g ` H )   =>    |- ( ( S e. (NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( [ X ] ( G ~QG S ) .+b [ Y ] ( G ~QG S ) ) = [ ( X .+ Y ) ] ( G ~QG S ) )
Theorem	qus0 13988	Value of the group identity operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.)
|- H = ( G /.s ( G ~QG S ) )   &    |- .0. = ( 0g ` G )   =>    |- ( S e. (NrmSGrp ` G ) -> [ .0. ] ( G ~QG S ) = ( 0g ` H ) )
Theorem	qusinv 13989	Value of the group inverse operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.)
|- H = ( G /.s ( G ~QG S ) )   &    |- V = ( Base ` G )   &    |- I = ( invg ` G )   &    |- N = ( invg ` H )   =>    |- ( ( S e. (NrmSGrp ` G ) /\ X e. V ) -> ( N ` [ X ] ( G ~QG S ) ) = [ ( I ` X ) ] ( G ~QG S ) )
Theorem	qussub 13990	Value of the group subtraction operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.)
|- H = ( G /.s ( G ~QG S ) )   &    |- V = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- N = ( -g ` H )   =>    |- ( ( S e. (NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( [ X ] ( G ~QG S ) N [ Y ] ( G ~QG S ) ) = [ ( X .- Y ) ] ( G ~QG S ) )
Theorem	ecqusaddd 13991	Addition of equivalence classes in a quotient group. (Contributed by AV, 25-Feb-2025.)
|- ( ph -> I e. (NrmSGrp ` R ) )   &    |- B = ( Base ` R )   &    |- .~ = ( R ~QG I )   &    |- Q = ( R /.s .~ )   =>    |- ( ( ph /\ ( A e. B /\ C e. B ) ) -> [ ( A ( +g ` R ) C ) ] .~ = ( [ A ] .~ ( +g ` Q ) [ C ] .~ ) )
Theorem	ecqusaddcl 13992	Closure of the addition in a quotient group. (Contributed by AV, 24-Feb-2025.)
|- ( ph -> I e. (NrmSGrp ` R ) )   &    |- B = ( Base ` R )   &    |- .~ = ( R ~QG I )   &    |- Q = ( R /.s .~ )   =>    |- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( [ A ] .~ ( +g ` Q ) [ C ] .~ ) e. ( Base ` Q ) )
7.2.4  Elementary theory of group homomorphisms
Syntax	cghm 13993	Extend class notation with the generator of group hom-sets.
class GrpHom
Definition	df-ghm 13994*	A homomorphism of groups is a map between two structures which preserves the group operation. Requiring both sides to be groups simplifies most theorems at the cost of complicating the theorem which pushes forward a group structure. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- GrpHom = ( s e. Grp , t e. Grp |-> { g | [. ( Base ` s ) / w ]. ( g : w --> ( Base ` t ) /\ A. x e. w A. y e. w ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) ) ) } )
Theorem	reldmghm 13995	Lemma for group homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- Rel dom GrpHom
Theorem	isghm 13996*	Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- X = ( Base ` S )   &    |- Y = ( Base ` T )   &    |- .+ = ( +g ` S )   &    |- .+^ = ( +g ` T )   =>    |- ( F e. ( S GrpHom T ) <-> ( ( S e. Grp /\ T e. Grp ) /\ ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) ) )
Theorem	isghm3 13997*	Property of a group homomorphism, similar to ismhm 13716. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- X = ( Base ` S )   &    |- Y = ( Base ` T )   &    |- .+ = ( +g ` S )   &    |- .+^ = ( +g ` T )   =>    |- ( ( S e. Grp /\ T e. Grp ) -> ( F e. ( S GrpHom T ) <-> ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) ) )
Theorem	ghmgrp1 13998	A group homomorphism is only defined when the domain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- ( F e. ( S GrpHom T ) -> S e. Grp )
Theorem	ghmgrp2 13999	A group homomorphism is only defined when the codomain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- ( F e. ( S GrpHom T ) -> T e. Grp )
Theorem	ghmf 14000	A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- X = ( Base ` S )   &    |- Y = ( Base ` T )   =>    |- ( F e. ( S GrpHom T ) -> F : X --> Y )