P. 171 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17001-17100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isabl 17001	The predicate "is an Abelian (commutative) group." (Contributed by NM, 17-Oct-2011.)
|- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
Theorem	ablgrp 17002	An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
|- ( G e. Abel -> G e. Grp )
Theorem	ablcmn 17003	An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. Abel -> G e. CMnd )
Theorem	iscmn 17004*	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 17005*	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 17006*	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 17007*	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 17008	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 17009*	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 17010*	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 17011*	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 17012	A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. CMnd -> G e. Mnd )
Theorem	cmncom 17013	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 17014	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 17015	Commutative/associative law for Abelian groups. (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 17016	Commutative/associative law for Abelian groups. (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 17017	Commutative/associative law for Abelian 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 17018	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	ablinvadd 17019	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 17020	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 17021	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 17022	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 17023	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 ) ) )
Theorem	abladdsub 17024	Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .- Z ) = ( ( X .- Z ) .+ Y ) )
Theorem	ablpncan2 17025	Cancellation law for subtraction. (Contributed by NM, 2-Oct-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) .- X ) = Y )
Theorem	ablpncan3 17026	A cancellation law for commutative groups. (Contributed by NM, 23-Mar-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> ( X .+ ( Y .- X ) ) = Y )
Theorem	ablsubsub 17027	Law for double subtraction. (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( X .- ( Y .- Z ) ) = ( ( X .- Y ) .+ Z ) )
Theorem	ablsubsub4 17028	Law for double subtraction. (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .- Z ) = ( X .- ( Y .+ Z ) ) )
Theorem	ablpnpcan 17029	Cancellation law for mixed addition and subtraction. (pnpcan 9849 analog.) (Contributed by NM, 29-May-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .+ Y ) .- ( X .+ Z ) ) = ( Y .- Z ) )
Theorem	ablnncan 17030	Cancellation law for group division. (nncan 9839 analog.) (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .- ( X .- Y ) ) = Y )
Theorem	ablsub32 17031	Swap the second and third terms in a double subtraction. (Contributed by NM, 7-Apr-2015.)
|- 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	ablnnncan1 17032	Cancellation law for subtraction. (nnncan1 9846 analog.) (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .- ( X .- Z ) ) = ( Z .- Y ) )
Theorem	mulgnn0di 17033	Group multiple of a sum, for nonnegative multiples. (Contributed by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) -> ( M .x. ( X .+ Y ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )
Theorem	mulgdi 17034	Group multiple of a sum. (Contributed by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( M .x. ( X .+ Y ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )
Theorem	mulgmhm 17035*	The map from x to n x for a fixed positive integer n is a monoid homomorphism if the monoid is commutative. (Contributed by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. CMnd /\ M e. NN0 ) -> ( x e. B |-> ( M .x. x ) ) e. ( G MndHom G ) )
Theorem	mulgghm 17036*	The map from x to n x for a fixed integer n is a group homomorphism if the group is commutative. (Contributed by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Abel /\ M e. ZZ ) -> ( x e. B |-> ( M .x. x ) ) e. ( G GrpHom G ) )
Theorem	mulgsubdi 17037	Group multiple of a difference. (Contributed by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( M .x. ( X .- Y ) ) = ( ( M .x. X ) .- ( M .x. Y ) ) )
Theorem	ghmfghm 17038*	The function fulfilling the conditions of ghmgrp 16393 is a group homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.)
|- X = ( Base ` G )   &    |- Y = ( Base ` H )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +g ` H )   &    |- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   &    |- ( ph -> F : X -onto-> Y )   &    |- ( ph -> G e. Grp )   =>    |- ( ph -> F e. ( G GrpHom H ) )
Theorem	ghmcmn 17039*	The image of a commutative monoid G under a group homomorphism F is a commutative monoid. (Contributed by Thierry Arnoux, 26-Jan-2020.)
|- X = ( Base ` G )   &    |- Y = ( Base ` H )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +g ` H )   &    |- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   &    |- ( ph -> F : X -onto-> Y )   &    |- ( ph -> G e. CMnd )   =>    |- ( ph -> H e. CMnd )
Theorem	ghmabl 17040*	The image of an abelian group G under a group homomorphism F is an abelian group. (Contributed by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.)
|- X = ( Base ` G )   &    |- Y = ( Base ` H )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +g ` H )   &    |- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   &    |- ( ph -> F : X -onto-> Y )   &    |- ( ph -> G e. Abel )   =>    |- ( ph -> H e. Abel )
Theorem	invghm 17041	The inversion map is a group automorphism if and only if the group is abelian. (In general it is only a group homomorphism into the opposite group, but in an abelian group the opposite group coincides with the group itself.) (Contributed by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` G )   &    |- I = ( invg ` G )   =>    |- ( G e. Abel <-> I e. ( G GrpHom G ) )
Theorem	eqgabl 17042	Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- X = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- .~ = ( G ~QG S )   =>    |- ( ( G e. Abel /\ S C_ X ) -> ( A .~ B <-> ( A e. X /\ B e. X /\ ( B .- A ) e. S ) ) )
Theorem	subgabl 17043	A subgroup of an abelian group is also abelian. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- H = ( G ↾s S )   =>    |- ( ( G e. Abel /\ S e. (SubGrp ` G ) ) -> H e. Abel )
Theorem	subcmn 17044	A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- H = ( G ↾s S )   =>    |- ( ( G e. CMnd /\ H e. Mnd ) -> H e. CMnd )
Theorem	submcmn 17045	A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- H = ( G ↾s S )   =>    |- ( ( G e. CMnd /\ S e. (SubMnd ` G ) ) -> H e. CMnd )
Theorem	submcmn2 17046	A submonoid is commutative iff it is a subset of its own centralizer. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- H = ( G ↾s S )   &    |- Z = (Cntz ` G )   =>    |- ( S e. (SubMnd ` G ) -> ( H e. CMnd <-> S C_ ( Z ` S ) ) )
Theorem	cntzcmn 17047	The centralizer of any subset in a commutative monoid is the whole monoid. (Contributed by Mario Carneiro, 3-Oct-2015.)
|- B = ( Base ` G )   &    |- Z = (Cntz ` G )   =>    |- ( ( G e. CMnd /\ S C_ B ) -> ( Z ` S ) = B )
Theorem	cntzcmnss 17048	Any subset in a commutative monoid is a subset of its centralizer. (Contributed by AV, 12-Jan-2019.)
|- B = ( Base ` G )   &    |- Z = (Cntz ` G )   =>    |- ( ( G e. CMnd /\ S C_ B ) -> S C_ ( Z ` S ) )
Theorem	cntzspan 17049	If the generators commute, the generated monoid is commutative. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- Z = (Cntz ` G )   &    |- K = (mrCls ` (SubMnd ` G ) )   &    |- H = ( G ↾s ( K ` S ) )   =>    |- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> H e. CMnd )
Theorem	cntzcmnf 17050	Discharge the centralizer assumption in a commutative monoid. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- B = ( Base ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ran F C_ ( Z ` ran F ) )
Theorem	ghmplusg 17051	The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- .+ = ( +g ` N )   =>    |- ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) -> ( F oF .+ G ) e. ( M GrpHom N ) )
Theorem	ablnsg 17052	Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( G e. Abel -> (NrmSGrp ` G ) = (SubGrp ` G ) )
Theorem	odadd1 17053	The order of a product in an abelian group divides the LCM of the orders of the factors. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- O = ( od ` G )   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` A ) x. ( O ` B ) ) )
Theorem	odadd2 17054	The order of a product in an abelian group is divisible by the LCM of the orders of the factors divided by the GCD. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- O = ( od ` G )   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` A ) x. ( O ` B ) ) || ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) )
Theorem	odadd 17055	The order of a product is the product of the orders, if the factors have coprime order. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- O = ( od ` G )   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( O ` ( A .+ B ) ) = ( ( O ` A ) x. ( O ` B ) ) )
Theorem	gex2abl 17056	A group with exponent 2 (or 1) is abelian. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- X = ( Base ` G )   &    |- E = (gEx ` G )   =>    |- ( ( G e. Grp /\ E || 2 ) -> G e. Abel )
Theorem	gexexlem 17057*	Lemma for gexex 17058. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- X = ( Base ` G )   &    |- E = (gEx ` G )   &    |- O = ( od ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> E e. NN )   &    |- ( ph -> A e. X )   &    |- ( ( ph /\ y e. X ) -> ( O ` y ) <_ ( O ` A ) )   =>    |- ( ph -> ( O ` A ) = E )
Theorem	gexex 17058*	In an abelian group with finite exponent, there is an element in the group with order equal to the exponent. In other words, all orders of elements divide the largest order of an element of the group. This fails if E = 0, for example in an infinite p-group, where there are elements of arbitrarily large orders (so E is zero) but no elements of infinite order. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- X = ( Base ` G )   &    |- E = (gEx ` G )   &    |- O = ( od ` G )   =>    |- ( ( G e. Abel /\ E e. NN ) -> E. x e. X ( O ` x ) = E )
Theorem	torsubg 17059	The set of all elements of finite order forms a subgroup of any abelian group, called the torsion subgroup. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- O = ( od ` G )   =>    |- ( G e. Abel -> ( `' O " NN ) e. (SubGrp ` G ) )
Theorem	oddvdssubg 17060*	The set of all elements whose order divides a fixed integer is a subgroup of any abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- O = ( od ` G )   &    |- B = ( Base ` G )   =>    |- ( ( G e. Abel /\ N e. ZZ ) -> { x e. B | ( O ` x ) || N } e. (SubGrp ` G ) )
Theorem	lsmcomx 17061	Subgroup sum commutes (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ( G e. Abel /\ T C_ B /\ U C_ B ) -> ( T .(+) U ) = ( U .(+) T ) )
Theorem	ablcntzd 17062	All subgroups in an abelian group commute. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- Z = (Cntz ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   =>    |- ( ph -> T C_ ( Z ` U ) )
Theorem	lsmcom 17063	Subgroup sum commutes. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( G e. Abel /\ T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> ( T .(+) U ) = ( U .(+) T ) )
Theorem	lsmsubg2 17064	The sum of two subgroups is a subgroup. (Contributed by NM, 4-Feb-2014.) (Proof shortened by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( G e. Abel /\ T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> ( T .(+) U ) e. (SubGrp ` G ) )
Theorem	lsm4 17065	Commutative/associative law for subgroup sum. (Contributed by NM, 26-Sep-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( G e. Abel /\ ( Q e. (SubGrp ` G ) /\ R e. (SubGrp ` G ) ) /\ ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) ) -> ( ( Q .(+) R ) .(+) ( T .(+) U ) ) = ( ( Q .(+) T ) .(+) ( R .(+) U ) ) )
Theorem	prdscmnd 17066	The product of a family of commutative monoids is commutative. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I -->CMnd )   =>    |- ( ph -> Y e. CMnd )
Theorem	prdsabld 17067	The product of a family of Abelian groups is an Abelian group. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Abel )   =>    |- ( ph -> Y e. Abel )
Theorem	pwscmn 17068	The structure power on a commutative monoid is commutative. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. CMnd /\ I e. V ) -> Y e. CMnd )
Theorem	pwsabl 17069	The structure power on an Abelian group is Abelian. (Contributed by Mario Carneiro, 21-Jan-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. Abel /\ I e. V ) -> Y e. Abel )
Theorem	qusabl 17070	If Y is a subgroup of the abelian group G, then H = G / Y is an abelian group. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- H = ( G /.s ( G ~QG S ) )   =>    |- ( ( G e. Abel /\ S e. (SubGrp ` G ) ) -> H e. Abel )
Theorem	abl1 17071	The (smallest) structure representing a trivial abelian group. (Contributed by AV, 28-Apr-2019.)
|- M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }   =>    |- ( I e. V -> M e. Abel )
Theorem	abln0 17072	Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019.)
|- Abel =/= (/)
Theorem	cnaddablx 17073	The complex numbers are an Abelian group under addition. This version of cnaddabl 17074 shows the explicit structure "scaffold" we chose for the definition for Abelian groups. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use cnaddabl 17074 instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012.)
|- G = { <. 1 , CC >. , <. 2 , + >. }   =>    |- G e. Abel
Theorem	cnaddabl 17074	The complex numbers are an Abelian group under addition. This version of cnaddablx 17073 hides the explicit structure indices i.e. is "scaffold-independent". Note that the proof also does not reference explicit structure indices. The actual structure is dependent on how Base and +g is defined. This theorem should not be referenced in any proof. For the group/ring properties of the complex numbers, see cnring 18635. (Contributed by NM, 20-Oct-2012.) (New usage is discouraged.)
|- G = { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. }   =>    |- G e. Abel
Theorem	zaddablx 17075	The integers are an Abelian group under addition. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. Use zsubrg 18666 instead. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.)
|- G = { <. 1 , ZZ >. , <. 2 , + >. }   =>    |- G e. Abel
Theorem	frgpnabllem1 17076*	Lemma for frgpnabl 17078. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- G = (freeGrp ` I )   &    |- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- .+ = ( +g ` G )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- U = (varFGrp ` I )   &    |- ( ph -> I e. _V )   &    |- ( ph -> A e. I )   &    |- ( ph -> B e. I )   =>    |- ( ph -> <" <. A , (/) >. <. B , (/) >. "> e. ( D i^i ( ( U ` A ) .+ ( U ` B ) ) ) )
Theorem	frgpnabllem2 17077*	Lemma for frgpnabl 17078. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- G = (freeGrp ` I )   &    |- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- .+ = ( +g ` G )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- U = (varFGrp ` I )   &    |- ( ph -> I e. _V )   &    |- ( ph -> A e. I )   &    |- ( ph -> B e. I )   &    |- ( ph -> ( ( U ` A ) .+ ( U ` B ) ) = ( ( U ` B ) .+ ( U ` A ) ) )   =>    |- ( ph -> A = B )
Theorem	frgpnabl 17078	The free group on two or more generators is not abelian. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- G = (freeGrp ` I )   =>    |- ( 1o ~< I -> -. G e. Abel )
10.3.2  Cyclic groups
Syntax	ccyg 17079	Cyclic group.
class CycGrp
Definition	df-cyg 17080*	Define a cyclic group, which is a group with an element x, called the generator of the group, such that all elements in the group are multiples of x. A generator is usually not unique. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- CycGrp = { g e. Grp | E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n (.g ` g ) x ) ) = ( Base ` g ) }
Theorem	iscyg 17081*	Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( G e. CycGrp <-> ( G e. Grp /\ E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = B ) )
Theorem	iscyggen 17082*	The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }   =>    |- ( X e. E <-> ( X e. B /\ ran ( n e. ZZ |-> ( n .x. X ) ) = B ) )
Theorem	iscyggen2 17083*	The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }   =>    |- ( G e. Grp -> ( X e. E <-> ( X e. B /\ A. y e. B E. n e. ZZ y = ( n .x. X ) ) ) )
Theorem	iscyg2 17084*	A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }   =>    |- ( G e. CycGrp <-> ( G e. Grp /\ E =/= (/) ) )
Theorem	cyggeninv 17085*	The inverse of a cyclic generator is a generator. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. E ) -> ( N ` X ) e. E )
Theorem	cyggenod 17086*	An element is the generator of a finite group iff the order of the generator equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }   &    |- O = ( od ` G )   =>    |- ( ( G e. Grp /\ B e. Fin ) -> ( X e. E <-> ( X e. B /\ ( O ` X ) = ( # ` B ) ) ) )
Theorem	cyggenod2 17087*	In an infinite cyclic group, the generator must have infinite order, but this property no longer characterizes the generators. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }   &    |- O = ( od ` G )   =>    |- ( ( G e. Grp /\ X e. E ) -> ( O ` X ) = if ( B e. Fin , ( # ` B ) , 0 ) )
Theorem	iscyg3 17088*	Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( G e. CycGrp <-> ( G e. Grp /\ E. x e. B A. y e. B E. n e. ZZ y = ( n .x. x ) ) )
Theorem	iscygd 17089*	Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   &    |- ( ( ph /\ y e. B ) -> E. n e. ZZ y = ( n .x. X ) )   =>    |- ( ph -> G e. CycGrp )
Theorem	iscygodd 17090	Show that a group with an element the same order as the group is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- B = ( Base ` G )   &    |- O = ( od ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   &    |- ( ph -> ( O ` X ) = ( # ` B ) )   =>    |- ( ph -> G e. CycGrp )
Theorem	cyggrp 17091	A cyclic group is a group. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- ( G e. CycGrp -> G e. Grp )
Theorem	cygabl 17092	A cyclic group is abelian. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- ( G e. CycGrp -> G e. Abel )
Theorem	cygctb 17093	A cyclic group is countable. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   =>    |- ( G e. CycGrp -> B ~<_ om )
Theorem	0cyg 17094	The trivial group is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   =>    |- ( ( G e. Grp /\ B ~~ 1o ) -> G e. CycGrp )
Theorem	prmcyg 17095	A group with prime order is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- B = ( Base ` G )   =>    |- ( ( G e. Grp /\ ( # ` B ) e. Prime ) -> G e. CycGrp )
Theorem	lt6abl 17096	A group with fewer than 6 elements is abelian. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- B = ( Base ` G )   =>    |- ( ( G e. Grp /\ ( # ` B ) < 6 ) -> G e. Abel )
Theorem	ghmcyg 17097	The image of a cyclic group under a surjective group homomorphism is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- C = ( Base ` H )   =>    |- ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) -> ( G e. CycGrp -> H e. CycGrp ) )
Theorem	cyggex2 17098	The exponent of a cyclic group is 0 if the group is infinite, otherwise it equals the order of the group. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- B = ( Base ` G )   &    |- E = (gEx ` G )   =>    |- ( G e. CycGrp -> E = if ( B e. Fin , ( # ` B ) , 0 ) )
Theorem	cyggex 17099	The exponent of a finite cyclic group is the order of the group. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- B = ( Base ` G )   &    |- E = (gEx ` G )   =>    |- ( ( G e. CycGrp /\ B e. Fin ) -> E = ( # ` B ) )
Theorem	cyggexb 17100	A finite abelian group is cyclic iff the exponent equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- E = (gEx ` G )   =>    |- ( ( G e. Abel /\ B e. Fin ) -> ( G e. CycGrp <-> E = ( # ` B ) ) )