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	ghmid 13801	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 13802	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 13803	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 13804*	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 13805	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 13806	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 13807	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 13808	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 13809	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 13810	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 13811	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 13812	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 13813	One direction of resghm2b 13814. (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 13814	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 13815	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 13816	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 13817	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 13818	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 13819	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 13820	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 13821	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 13822	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 13823	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 13824	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 13825*	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 13826	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 13827	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 13828*	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 13829*	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 13830*	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 13831*	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 13832*	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 13833*	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 13834*	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 13835*	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 13836	Extend class notation with class of all commutative monoids.
class CMnd
Syntax	cabl 13837	Extend class notation with class of all Abelian groups.
class Abel
Definition	df-cmn 13838*	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 13839	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 13840	The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.)
|- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
Theorem	ablgrp 13841	An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
|- ( G e. Abel -> G e. Grp )
Theorem	ablgrpd 13842	An Abelian group is a group, deduction form of ablgrp 13841. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- ( ph -> G e. Abel )   =>    |- ( ph -> G e. Grp )
Theorem	ablcmn 13843	An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. Abel -> G e. CMnd )
Theorem	ablcmnd 13844	An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
|- ( ph -> G e. Abel )   =>    |- ( ph -> G e. CMnd )
Theorem	iscmn 13845*	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 13846*	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 13847*	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 13848*	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 13849	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 13850*	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 13851*	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 13852*	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 13853	A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. CMnd -> G e. Mnd )
Theorem	cmncom 13854	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 13855	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 13856	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 13857	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 13858	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 13859	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 13860	A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.)
|- ( ph -> G e. CMnd )   =>    |- ( ph -> G e. Mnd )
Theorem	rinvmod 13861*	Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovimo 6205. (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 13862	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 13863	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 13864	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 13865	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 13866	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 13867	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 13868	Cancellation law for subtraction in an Abelian group. (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 13869	A cancellation law for Abelian 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 13870	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 13871	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 13872	Cancellation law for mixed addition and subtraction. (pnpcan 8396 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 13873	Cancellation law for group subtraction. (nncan 8386 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 13874	Swap the second and third terms in a double group 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	ablnnncan 13875	Cancellation law for group subtraction. (nnncan 8392 analog.) (Contributed by NM, 29-Feb-2008.) (Revised by AV, 27-Aug-2021.)
|- 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 ) ) .- Z ) = ( X .- Y ) )
Theorem	ablnnncan1 13876	Cancellation law for group subtraction. (nnncan1 8393 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	ablsubsub23 13877	Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007.) (Revised by AV, 7-Oct-2021.)
|- V = ( Base ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) = C <-> ( A .- C ) = B ) )
Theorem	ghmfghm 13878*	The function fulfilling the conditions of ghmgrp 13670 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 13879*	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 13880*	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 13881	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 13882	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	qusecsub 13883	Two subgroup cosets are equal if and only if the difference of their representatives is a member of the subgroup. (Contributed by AV, 7-Mar-2025.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- .~ = ( G ~QG S )   =>    |- ( ( ( G e. Abel /\ S e. (SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( [ X ] .~ = [ Y ] .~ <-> ( Y .- X ) e. S ) )
Theorem	subgabl 13884	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	subcmnd 13885	A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- ( ph -> H = ( G ↾s S ) )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> S e. V )   =>    |- ( ph -> H e. CMnd )
Theorem	ablnsg 13886	Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( G e. Abel -> (NrmSGrp ` G ) = (SubGrp ` G ) )
Theorem	ablressid 13887	A commutative group restricted to its base set is a commutative group. It will usually be the original group exactly, of course, but to show that needs additional conditions such as those in strressid 13119. (Contributed by Jim Kingdon, 5-May-2025.)
|- B = ( Base ` G )   =>    |- ( G e. Abel -> ( G ↾s B ) e. Abel )
Theorem	imasabl 13888*	The image structure of an abelian group is an abelian group (imasgrp 13663 analog). (Contributed by AV, 22-Feb-2025.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .+ = ( +g ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )   &    |- ( ph -> R e. Abel )   &    |- .0. = ( 0g ` R )   =>    |- ( ph -> ( U e. Abel /\ ( F ` .0. ) = ( 0g ` U ) ) )
7.2.5.2  Group sum operation
Theorem	gsumfzreidx 13889	Re-index a finite group sum using a bijection. Corresponds to the first equation in [Lang] p. 5 with M = 1. (Contributed by AV, 26-Dec-2023.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> F : ( M ... N ) --> B )   &    |- ( ph -> H : ( M ... N ) -1-1-onto-> ( M ... N ) )   =>    |- ( ph -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) )
Theorem	gsumfzsubmcl 13890	Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 30-Aug-2025.)
|- ( ph -> G e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> S e. (SubMnd ` G ) )   &    |- ( ph -> F : ( M ... N ) --> S )   =>    |- ( ph -> ( G gsumg F ) e. S )
Theorem	gsumfzmptfidmadd 13891*	The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019.) (Revised by Jim Kingdon, 31-Aug-2025.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> C e. B )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> D e. B )   &    |- F = ( x e. ( M ... N ) |-> C )   &    |- H = ( x e. ( M ... N ) |-> D )   =>    |- ( ph -> ( G gsumg ( x e. ( M ... N ) |-> ( C .+ D ) ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
Theorem	gsumfzmptfidmadd2 13892*	The sum of two group sums expressed as mappings with finite domain, using a function operation. (Contributed by AV, 23-Jul-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> C e. B )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> D e. B )   &    |- F = ( x e. ( M ... N ) |-> C )   &    |- H = ( x e. ( M ... N ) |-> D )   =>    |- ( ph -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
Theorem	gsumfzconst 13893*	Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Jim Kingdon, 6-Sep-2025.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mnd /\ N e. ( ZZ>= ` M ) /\ X e. B ) -> ( G gsumg ( k e. ( M ... N ) |-> X ) ) = ( ( ( N - M ) + 1 ) .x. X ) )
Theorem	gsumfzconstf 13894*	Sum of a constant series. (Contributed by Thierry Arnoux, 5-Jul-2017.)
|- F/_ k X   &    |- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mnd /\ N e. ( ZZ>= ` M ) /\ X e. B ) -> ( G gsumg ( k e. ( M ... N ) |-> X ) ) = ( ( ( N - M ) + 1 ) .x. X ) )
Theorem	gsumfzmhm 13895	Apply a monoid homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 8-Sep-2025.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> K e. ( G MndHom H ) )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( H gsumg ( K o. F ) ) = ( K ` ( G gsumg F ) ) )
Theorem	gsumfzmhm2 13896*	Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 9-Sep-2025.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> ( x e. B |-> C ) e. ( G MndHom H ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> X e. B )   &    |- ( x = X -> C = D )   &    |- ( x = ( G gsumg ( k e. ( M ... N ) |-> X ) ) -> C = E )   =>    |- ( ph -> ( H gsumg ( k e. ( M ... N ) |-> D ) ) = E )
Theorem	gsumfzsnfd 13897*	Group sum of a singleton, deduction form, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Revised by AV, 11-Dec-2019.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> C e. B )   &    |- ( ( ph /\ k = M ) -> A = C )   &    |- F/ k ph   &    |- F/_ k C   =>    |- ( ph -> ( G gsumg ( k e. { M } |-> A ) ) = C )
7.3  Rings
7.3.1  Multiplicative Group
Syntax	cmgp 13898	Multiplicative group.
class mulGrp
Definition	df-mgp 13899	Define a structure that puts the multiplication operation of a ring in the addition slot. Note that this will not actually be a group for the average ring, or even for a field, but it will be a monoid, and we get a group if we restrict to the elements that have inverses. This allows us to formalize such notions as "the multiplication operation of a ring is a monoid" or "the multiplicative identity" in terms of the identity of a monoid (df-ur 13938). (Contributed by Mario Carneiro, 21-Dec-2014.)
|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
Theorem	fnmgp 13900	The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- mulGrp Fn _V