P. 139 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13801-13900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nsgid 13801	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 13802	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 13803	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 13804	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 13805	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 13806	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 13807	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 13808*	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 13809	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 13810	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 13811*	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 13812	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 13813	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 13814	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 13815	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 13816*	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 13817	Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) Generalization of quseccl 13819 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 13818	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 13819	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 13820	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 13821	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 13822	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 13823	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 13824	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 13825	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 13826	Extend class notation with the generator of group hom-sets.
class GrpHom
Definition	df-ghm 13827*	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 13828	Lemma for group homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.)
|- Rel dom GrpHom
Theorem	isghm 13829*	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 13830*	Property of a group homomorphism, similar to ismhm 13543. (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 13831	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 13832	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 13833	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 13834	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 13835	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 13836	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 13837	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 13838*	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 13839	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 13840	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 13841	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 13842	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 13843	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 13844	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 13845	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 13846	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 13847	One direction of resghm2b 13848. (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 13848	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 13849	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 13850	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 13851	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 13852	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 13853	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 13854	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 13855	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 13856	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 13857	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 13858	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 13859*	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 13860	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 13861	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 13862*	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 13863*	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 13864*	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 13865*	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 13866*	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 13867*	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 13868*	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 13869*	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 13870	Extend class notation with class of all commutative monoids.
class CMnd
Syntax	cabl 13871	Extend class notation with class of all Abelian groups.
class Abel
Definition	df-cmn 13872*	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 13873	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 13874	The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.)
|- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
Theorem	ablgrp 13875	An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
|- ( G e. Abel -> G e. Grp )
Theorem	ablgrpd 13876	An Abelian group is a group, deduction form of ablgrp 13875. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- ( ph -> G e. Abel )   =>    |- ( ph -> G e. Grp )
Theorem	ablcmn 13877	An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. Abel -> G e. CMnd )
Theorem	ablcmnd 13878	An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
|- ( ph -> G e. Abel )   =>    |- ( ph -> G e. CMnd )
Theorem	iscmn 13879*	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 13880*	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 13881*	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 13882*	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 13883	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 )
Theorem	iscmnd 13884*	Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> G e. Mnd )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- ( ph -> G e. CMnd )
Theorem	isabld 13885*	Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> G e. Grp )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- ( ph -> G e. Abel )
Theorem	isabli 13886*	Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.)
|- G e. Grp   &    |- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ( x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- G e. Abel
Theorem	cmnmnd 13887	A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. CMnd -> G e. Mnd )
Theorem	cmncom 13888	A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	ablcom 13889	An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	cmn32 13890	Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Z ) .+ Y ) )
Theorem	cmn4 13891	Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( ( X .+ Z ) .+ ( Y .+ W ) ) )
Theorem	cmn12 13892	Commutative/associative law for commutative monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .+ ( Y .+ Z ) ) = ( Y .+ ( X .+ Z ) ) )
Theorem	abl32 13893	Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Z ) .+ Y ) )
Theorem	cmnmndd 13894	A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.)
|- ( ph -> G e. CMnd )   =>    |- ( ph -> G e. Mnd )
Theorem	rinvmod 13895*	Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovimo 6215. (Contributed by AV, 31-Dec-2023.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. B )   =>    |- ( ph -> E* w e. B ( A .+ w ) = .0. )
Theorem	ablinvadd 13896	The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( N ` ( X .+ Y ) ) = ( ( N ` X ) .+ ( N ` Y ) ) )
Theorem	ablsub2inv 13897	Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- N = ( invg ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) .- ( N ` Y ) ) = ( Y .- X ) )
Theorem	ablsubadd 13898	Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) = Z <-> ( Y .+ Z ) = X ) )
Theorem	ablsub4 13899	Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .- ( Z .+ W ) ) = ( ( X .- Z ) .+ ( Y .- W ) ) )
Theorem	abladdsub4 13900	Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) = ( Z .+ W ) <-> ( X .- Z ) = ( W .- Y ) ) )