P. 141 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14001-14100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subgintm 14001*	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 14002	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 14003	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 14004	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 14005*	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 14006*	Weaken the condition of isnsg 14005 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 14007	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 14008	A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- ( S e. (NrmSGrp ` G ) -> S e. (SubGrp ` G ) )
Theorem	nsgconj 14009	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 14010*	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 14011*	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 14012*	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 14013*	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 14014*	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 14015*	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 14016*	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 14017	The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> { .0. } e. (NrmSGrp ` G ) )
Theorem	nsgid 14018	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 14019	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 14020	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 14021	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 14022	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 14023	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 14024	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 14025*	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 14026	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 14027	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 14028*	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 14029	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 14030	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 14031	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 14032	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 14033*	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 14034	Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) Generalization of quseccl 14036 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 14035	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 14036	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 14037	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 14038	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 14039	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 14040	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 14041	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 14042	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 14043	Extend class notation with the generator of group hom-sets.
class GrpHom
Definition	df-ghm 14044*	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 14045	Lemma for group homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- Rel dom GrpHom
Theorem	isghm 14046*	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 14047*	Property of a group homomorphism, similar to ismhm 13768. (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 14048	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 14049	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 14050	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 )
Theorem	ghmlin 14051	A homomorphism of groups is linear. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- X = ( Base ` S )   &    |- .+ = ( +g ` S )   &    |- .+^ = ( +g ` T )   =>    |- ( ( F e. ( S GrpHom T ) /\ U e. X /\ V e. X ) -> ( F ` ( U .+ V ) ) = ( ( F ` U ) .+^ ( F ` V ) ) )
Theorem	ghmid 14052	A homomorphism of groups preserves the identity. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- Y = ( 0g ` S )   &    |- .0. = ( 0g ` T )   =>    |- ( F e. ( S GrpHom T ) -> ( F ` Y ) = .0. )
Theorem	ghminv 14053	A homomorphism of groups preserves inverses. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- B = ( Base ` S )   &    |- M = ( invg ` S )   &    |- N = ( invg ` T )   =>    |- ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( F ` ( M ` X ) ) = ( N ` ( F ` X ) ) )
Theorem	ghmsub 14054	Linearity of subtraction through a group homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- B = ( Base ` S )   &    |- .- = ( -g ` S )   &    |- N = ( -g ` T )   =>    |- ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( F ` ( U .- V ) ) = ( ( F ` U ) N ( F ` V ) ) )
Theorem	isghmd 14055*	Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.)
|- X = ( Base ` S )   &    |- Y = ( Base ` T )   &    |- .+ = ( +g ` S )   &    |- .+^ = ( +g ` T )   &    |- ( ph -> S e. Grp )   &    |- ( ph -> T e. Grp )   &    |- ( ph -> F : X --> Y )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   =>    |- ( ph -> F e. ( S GrpHom T ) )
Theorem	ghmmhm 14056	A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( S GrpHom T ) -> F e. ( S MndHom T ) )
Theorem	ghmmhmb 14057	Group homomorphisms and monoid homomorphisms coincide. (Thus, GrpHom is somewhat redundant, although its stronger reverse closure properties are sometimes useful.) (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( ( S e. Grp /\ T e. Grp ) -> ( S GrpHom T ) = ( S MndHom T ) )
Theorem	ghmex 14058	The set of group homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.)
|- ( ( S e. Grp /\ T e. Grp ) -> ( S GrpHom T ) e. _V )
Theorem	ghmmulg 14059	A group homomorphism preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .X. = (.g ` H )   =>    |- ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )
Theorem	ghmrn 14060	The range of a homomorphism is a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- ( F e. ( S GrpHom T ) -> ran F e. (SubGrp ` T ) )
Theorem	0ghm 14061	The constant zero linear function between two groups. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- .0. = ( 0g ` N )   &    |- B = ( Base ` M )   =>    |- ( ( M e. Grp /\ N e. Grp ) -> ( B X. { .0. } ) e. ( M GrpHom N ) )
Theorem	idghm 14062	The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- B = ( Base ` G )   =>    |- ( G e. Grp -> ( _I |` B ) e. ( G GrpHom G ) )
Theorem	resghm 14063	Restriction of a homomorphism to a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- U = ( S ↾s X )   =>    |- ( ( F e. ( S GrpHom T ) /\ X e. (SubGrp ` S ) ) -> ( F |` X ) e. ( U GrpHom T ) )
Theorem	resghm2 14064	One direction of resghm2b 14065. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.)
|- U = ( T ↾s X )   =>    |- ( ( F e. ( S GrpHom U ) /\ X e. (SubGrp ` T ) ) -> F e. ( S GrpHom T ) )
Theorem	resghm2b 14065	Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.)
|- U = ( T ↾s X )   =>    |- ( ( X e. (SubGrp ` T ) /\ ran F C_ X ) -> ( F e. ( S GrpHom T ) <-> F e. ( S GrpHom U ) ) )
Theorem	ghmghmrn 14066	A group homomorphism from G to H is also a group homomorphism from G to its image in H. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by AV, 26-Aug-2021.)
|- U = ( T ↾s ran F )   =>    |- ( F e. ( S GrpHom T ) -> F e. ( S GrpHom U ) )
Theorem	ghmco 14067	The composition of group homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- ( ( F e. ( T GrpHom U ) /\ G e. ( S GrpHom T ) ) -> ( F o. G ) e. ( S GrpHom U ) )
Theorem	ghmima 14068	The image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- ( ( F e. ( S GrpHom T ) /\ U e. (SubGrp ` S ) ) -> ( F " U ) e. (SubGrp ` T ) )
Theorem	ghmpreima 14069	The inverse image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- ( ( F e. ( S GrpHom T ) /\ V e. (SubGrp ` T ) ) -> ( `' F " V ) e. (SubGrp ` S ) )
Theorem	ghmeql 14070	The equalizer of two group homomorphisms is a subgroup. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> dom ( F i^i G ) e. (SubGrp ` S ) )
Theorem	ghmnsgima 14071	The image of a normal subgroup under a surjective homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- Y = ( Base ` T )   =>    |- ( ( F e. ( S GrpHom T ) /\ U e. (NrmSGrp ` S ) /\ ran F = Y ) -> ( F " U ) e. (NrmSGrp ` T ) )
Theorem	ghmnsgpreima 14072	The inverse image of a normal subgroup under a homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( F e. ( S GrpHom T ) /\ V e. (NrmSGrp ` T ) ) -> ( `' F " V ) e. (NrmSGrp ` S ) )
Theorem	ghmker 14073	The kernel of a homomorphism is a normal subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- .0. = ( 0g ` T )   =>    |- ( F e. ( S GrpHom T ) -> ( `' F " { .0. } ) e. (NrmSGrp ` S ) )
Theorem	ghmeqker 14074	Two source points map to the same destination point under a group homomorphism iff their difference belongs to the kernel. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- B = ( Base ` S )   &    |- .0. = ( 0g ` T )   &    |- K = ( `' F " { .0. } )   &    |- .- = ( -g ` S )   =>    |- ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( F ` U ) = ( F ` V ) <-> ( U .- V ) e. K ) )
Theorem	f1ghm0to0 14075	If a group homomorphism F is injective, it maps the zero of one group (and only the zero) to the zero of the other group. (Contributed by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 13-May-2023.)
|- A = ( Base ` R )   &    |- B = ( Base ` S )   &    |- N = ( 0g ` R )   &    |- .0. = ( 0g ` S )   =>    |- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( ( F ` X ) = .0. <-> X = N ) )
Theorem	ghmf1 14076*	Two ways of saying a group homomorphism is 1-1 into its codomain. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) (Proof shortened by AV, 4-Apr-2025.)
|- A = ( Base ` R )   &    |- B = ( Base ` S )   &    |- N = ( 0g ` R )   &    |- .0. = ( 0g ` S )   =>    |- ( F e. ( R GrpHom S ) -> ( F : A -1-1-> B <-> A. x e. A ( ( F ` x ) = .0. -> x = N ) ) )
Theorem	kerf1ghm 14077	A group homomorphism F is injective if and only if its kernel is the singleton { N }. (Contributed by Thierry Arnoux, 27-Oct-2017.) (Proof shortened by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 13-May-2023.)
|- A = ( Base ` R )   &    |- B = ( Base ` S )   &    |- N = ( 0g ` R )   &    |- .0. = ( 0g ` S )   =>    |- ( F e. ( R GrpHom S ) -> ( F : A -1-1-> B <-> ( `' F " { .0. } ) = { N } ) )
Theorem	ghmf1o 14078	A bijective group homomorphism is an isomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` S )   &    |- Y = ( Base ` T )   =>    |- ( F e. ( S GrpHom T ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( T GrpHom S ) ) )
Theorem	conjghm 14079*	Conjugation is an automorphism of the group. (Contributed by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- F = ( x e. X |-> ( ( A .+ x ) .- A ) )   =>    |- ( ( G e. Grp /\ A e. X ) -> ( F e. ( G GrpHom G ) /\ F : X -1-1-onto-> X ) )
Theorem	conjsubg 14080*	A conjugated subgroup is also a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- F = ( x e. S |-> ( ( A .+ x ) .- A ) )   =>    |- ( ( S e. (SubGrp ` G ) /\ A e. X ) -> ran F e. (SubGrp ` G ) )
Theorem	conjsubgen 14081*	A conjugated subgroup is equinumerous to the original subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- F = ( x e. S |-> ( ( A .+ x ) .- A ) )   =>    |- ( ( S e. (SubGrp ` G ) /\ A e. X ) -> S ~~ ran F )
Theorem	conjnmz 14082*	A subgroup is unchanged under conjugation by an element of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- F = ( x e. S |-> ( ( A .+ x ) .- A ) )   &    |- N = { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) }   =>    |- ( ( S e. (SubGrp ` G ) /\ A e. N ) -> S = ran F )
Theorem	conjnmzb 14083*	Alternative condition for elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- F = ( x e. S |-> ( ( A .+ x ) .- A ) )   &    |- N = { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) }   =>    |- ( S e. (SubGrp ` G ) -> ( A e. N <-> ( A e. X /\ S = ran F ) ) )
Theorem	conjnsg 14084*	A normal subgroup is unchanged under conjugation. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- F = ( x e. S |-> ( ( A .+ x ) .- A ) )   =>    |- ( ( S e. (NrmSGrp ` G ) /\ A e. X ) -> S = ran F )
Theorem	qusghm 14085*	If Y is a normal subgroup of G, then the "natural map" from elements to their cosets is a group homomorphism from G to G / Y. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 18-Sep-2015.)
|- X = ( Base ` G )   &    |- H = ( G /.s ( G ~QG Y ) )   &    |- F = ( x e. X |-> [ x ] ( G ~QG Y ) )   =>    |- ( Y e. (NrmSGrp ` G ) -> F e. ( G GrpHom H ) )
Theorem	ghmpropd 14086*	Group homomorphism depends only on the group attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- ( ph -> B = ( Base ` J ) )   &    |- ( ph -> C = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> C = ( Base ` M ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )   =>    |- ( ph -> ( J GrpHom K ) = ( L GrpHom M ) )
7.2.5  Abelian groups
7.2.5.1  Definition and basic properties
Syntax	ccmn 14087	Extend class notation with class of all commutative monoids.
class CMnd
Syntax	cabl 14088	Extend class notation with class of all Abelian groups.
class Abel
Definition	df-cmn 14089*	Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
Definition	df-abl 14090	Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- Abel = ( Grp i^i CMnd )
Theorem	isabl 14091	The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.)
|- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
Theorem	ablgrp 14092	An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
|- ( G e. Abel -> G e. Grp )
Theorem	ablgrpd 14093	An Abelian group is a group, deduction form of ablgrp 14092. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- ( ph -> G e. Abel )   =>    |- ( ph -> G e. Grp )
Theorem	ablcmn 14094	An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. Abel -> G e. CMnd )
Theorem	ablcmnd 14095	An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
|- ( ph -> G e. Abel )   =>    |- ( ph -> G e. CMnd )
Theorem	iscmn 14096*	The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. CMnd <-> ( G e. Mnd /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
Theorem	isabl2 14097*	The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Abel <-> ( G e. Grp /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
Theorem	cmnpropd 14098*	If two structures have the same group components (properties), one is a commutative monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-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 -> ( K e. CMnd <-> L e. CMnd ) )
Theorem	ablpropd 14099*	If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 6-Dec-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( K e. Abel <-> L e. Abel ) )
Theorem	ablprop 14100	If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 11-Oct-2013.)
|- ( Base ` K ) = ( Base ` L )   &    |- ( +g ` K ) = ( +g ` L )   =>    |- ( K e. Abel <-> L e. Abel )