P. 255 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25401-25500   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-ablo 25401*	Define the class of all Abelian group operations. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
|- AbelOp = { g e. GrpOp | A. x e. ran g A. y e. ran g ( x g y ) = ( y g x ) }
Theorem	isablo 25402*	The predicate "is an Abelian (commutative) group operation." (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
|- X = ran G   =>    |- ( G e. AbelOp <-> ( G e. GrpOp /\ A. x e. X A. y e. X ( x G y ) = ( y G x ) ) )
Theorem	ablogrpo 25403	An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
|- ( G e. AbelOp -> G e. GrpOp )
Theorem	ablocom 25404	An Abelian group operation is commutative. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
|- X = ran G   =>    |- ( ( G e. AbelOp /\ A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) )
Theorem	ablo32 25405	Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.)
|- X = ran G   =>    |- ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( ( A G C ) G B ) )
Theorem	ablo4 25406	Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.)
|- X = ran G   =>    |- ( ( G e. AbelOp /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( C G D ) ) = ( ( A G C ) G ( B G D ) ) )
Theorem	isabloi 25407*	Properties that determine an Abelian group operation. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.)
|- G e. GrpOp   &    |- dom G = ( X X. X )   &    |- ( ( x e. X /\ y e. X ) -> ( x G y ) = ( y G x ) )   =>    |- G e. AbelOp
Theorem	ablomuldiv 25408	Law for group multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
|- X = ran G   &    |- D = ( /g ` G )   =>    |- ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) D C ) = ( ( A D C ) G B ) )
Theorem	ablodivdiv 25409	Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.)
|- X = ran G   &    |- D = ( /g ` G )   =>    |- ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D ( B D C ) ) = ( ( A D B ) G C ) )
Theorem	ablodivdiv4 25410	Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.)
|- X = ran G   &    |- D = ( /g ` G )   =>    |- ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) D C ) = ( A D ( B G C ) ) )
Theorem	ablodiv32 25411	Swap the second and third terms in a double division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.)
|- X = ran G   &    |- D = ( /g ` G )   =>    |- ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) D C ) = ( ( A D C ) D B ) )
Theorem	ablonnncan 25412	Cancellation law for group division. (nnncan 9767 analog.) (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.)
|- X = ran G   &    |- D = ( /g ` G )   =>    |- ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D ( B D C ) ) D C ) = ( A D B ) )
Theorem	ablonncan 25413	Cancellation law for group division. (nncan 9761 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.)
|- X = ran G   &    |- D = ( /g ` G )   =>    |- ( ( G e. AbelOp /\ A e. X /\ B e. X ) -> ( A D ( A D B ) ) = B )
Theorem	ablonnncan1 25414	Cancellation law for group division. (nnncan1 9768 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.)
|- X = ran G   &    |- D = ( /g ` G )   =>    |- ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) D ( A D C ) ) = ( C D B ) )
Theorem	gxdi 25415	Distribution of group power over group operation for abelian groups. (Contributed by Paul Chapman, 17-Apr-2009.) (New usage is discouraged.)
|- X = ran G   &    |- P = ( ^g ` G )   =>    |- ( ( G e. AbelOp /\ ( A e. X /\ B e. X ) /\ K e. ZZ ) -> ( ( A G B ) P K ) = ( ( A P K ) G ( B P K ) ) )
Theorem	isgrpda 25416*	Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009.) (New usage is discouraged.)
|- ( ph -> X e. _V )   &    |- ( ph -> G : ( X X. X ) --> X )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) )   &    |- ( ph -> U e. X )   &    |- ( ( ph /\ x e. X ) -> ( U G x ) = x )   &    |- ( ( ph /\ x e. X ) -> E. n e. X ( n G x ) = U )   =>    |- ( ph -> G e. GrpOp )
Theorem	isgrpod 25417*	Properties that determine a group operation. (Renamed from isgrpd 16192 to isgrpod 25417 to prevent naming conflict. -NM 5-Jun-2013) (Contributed by Jeff Madsen, 1-Dec-2009.) (New usage is discouraged.)
|- ( ph -> X e. _V )   &    |- ( ph -> G : ( X X. X ) --> X )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) )   &    |- ( ph -> U e. X )   &    |- ( ( ph /\ x e. X ) -> ( U G x ) = x )   &    |- ( ( ph /\ x e. X ) -> N e. X )   &    |- ( ( ph /\ x e. X ) -> ( N G x ) = U )   =>    |- ( ph -> G e. GrpOp )
Theorem	isabloda 25418*	Properties that determine an Abelian group operation. (Contributed by Jeff Madsen, 11-Jun-2010.) (New usage is discouraged.)
|- ( ph -> X e. _V )   &    |- ( ph -> G : ( X X. X ) --> X )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) )   &    |- ( ph -> U e. X )   &    |- ( ( ph /\ x e. X ) -> ( U G x ) = x )   &    |- ( ( ph /\ x e. X ) -> E. n e. X ( n G x ) = U )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x G y ) = ( y G x ) )   =>    |- ( ph -> G e. AbelOp )
Theorem	isablod 25419*	Properties that determine an Abelian group operation. (Changed label from isabld 16928 to isablod 25419-NM 6-Aug-2013.) (Contributed by Jeff Madsen, 5-Dec-2009.) (New usage is discouraged.)
|- ( ph -> X e. _V )   &    |- ( ph -> G : ( X X. X ) --> X )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) )   &    |- ( ph -> U e. X )   &    |- ( ( ph /\ x e. X ) -> ( U G x ) = x )   &    |- ( ( ph /\ x e. X ) -> N e. X )   &    |- ( ( ph /\ x e. X ) -> ( N G x ) = U )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x G y ) = ( y G x ) )   =>    |- ( ph -> G e. AbelOp )
18.1.3  Subgroups
Syntax	csubgo 25420	Extend class notation to include the class of subgroups.
class SubGrpOp
Definition	df-subgo 25421	Define the set of subgroups of g. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.)
|- SubGrpOp = ( g e. GrpOp |-> ( GrpOp i^i ~P g ) )
Theorem	issubgo 25422	The predicate "is a subgroup of G." (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 12-Jul-2014.) (New usage is discouraged.)
|- ( H e. ( SubGrpOp ` G ) <-> ( G e. GrpOp /\ H e. GrpOp /\ H C_ G ) )
Theorem	subgores 25423	A subgroup operation is the restriction of its parent group operation to its underlying set. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.)
|- W = ran H   =>    |- ( H e. ( SubGrpOp ` G ) -> H = ( G |` ( W X. W ) ) )
Theorem	subgoov 25424	The result of a subgroup operation is the same as the result of its parent operation. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 8-Jul-2014.) (New usage is discouraged.)
|- W = ran H   =>    |- ( ( H e. ( SubGrpOp ` G ) /\ ( A e. W /\ B e. W ) ) -> ( A H B ) = ( A G B ) )
Theorem	subgornss 25425	The underlying set of a subgroup is a subset of its parent group's underlying set. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.)
|- X = ran G   &    |- W = ran H   =>    |- ( H e. ( SubGrpOp ` G ) -> W C_ X )
Theorem	subgoid 25426	The identity element of a subgroup is the same as its parent's. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.)
|- U = (GId ` G )   &    |- T = (GId ` H )   =>    |- ( H e. ( SubGrpOp ` G ) -> T = U )
Theorem	subgoinv 25427	The inverse of a subgroup element is the same as its inverse in the parent group. (Contributed by Mario Carneiro, 8-Jul-2014.) (New usage is discouraged.)
|- W = ran H   &    |- M = ( inv ` G )   &    |- N = ( inv ` H )   =>    |- ( ( H e. ( SubGrpOp ` G ) /\ A e. W ) -> ( N ` A ) = ( M ` A ) )
Theorem	issubgoilem 25428*	Lemma for issubgoi 25429. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
|- ( ( x e. Y /\ y e. Y ) -> ( x H y ) = ( x G y ) )   =>    |- ( ( A e. Y /\ B e. Y ) -> ( A H B ) = ( A G B ) )
Theorem	issubgoi 25429*	Properties that determine a subgroup. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
|- G e. GrpOp   &    |- X = ran G   &    |- U = (GId ` G )   &    |- N = ( inv ` G )   &    |- Y C_ X   &    |- H = ( G |` ( Y X. Y ) )   &    |- ( ( x e. Y /\ y e. Y ) -> ( x G y ) e. Y )   &    |- U e. Y   &    |- ( x e. Y -> ( N ` x ) e. Y )   =>    |- H e. ( SubGrpOp ` G )
Theorem	subgoablo 25430	A subgroup of an Abelian group is Abelian. (Contributed by Paul Chapman, 25-Apr-2008.) (New usage is discouraged.)
|- ( ( G e. AbelOp /\ H e. ( SubGrpOp ` G ) ) -> H e. AbelOp )
18.1.4  Operation properties
Syntax	cass 25431	Extend class notation with a device to add associativity to internal operations.
class Ass
Definition	df-ass 25432*	A device to add associativity to various sorts of internal operations. The definition is meaningful when g is a magma at least. (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
|- Ass = { g | A. x e. dom dom g A. y e. dom dom g A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) ) }
Syntax	cexid 25433	Extend class notation with the class of all the internal operations with an identity element.
class ExId
Definition	df-exid 25434*	A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- ExId = { g | E. x e. dom dom g A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y ) }
Theorem	isass 25435*	The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
|- X = dom dom G   =>    |- ( G e. A -> ( G e. Ass <-> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
Theorem	isexid 25436*	The predicate G has a left and right identity element. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = dom dom G   =>    |- ( G e. A -> ( G e. ExId <-> E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) )
18.1.5  Group-like structures
Syntax	cmagm 25437	Extend class notation with the class of all magmas.
class Magma
Definition	df-mgmOLD 25438*	Obsolete version of df-mgm 15989 as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- Magma = { g | E. t g : ( t X. t ) --> t }
Theorem	ismgmOLD 25439	Obsolete version of ismgm 15990 as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = dom dom G   =>    |- ( G e. A -> ( G e. Magma <-> G : ( X X. X ) --> X ) )
Theorem	clmgmOLD 25440	Obsolete version of mgmcl 15992 as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = dom dom G   =>    |- ( ( G e. Magma /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
Theorem	opidonOLD 25441	Obsolete version of mndpfo 16061 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = dom dom G   =>    |- ( G e. ( Magma i^i ExId ) -> G : ( X X. X ) -onto-> X )
Theorem	rngopidOLD 25442	Obsolete version of mndpfo 16061 as of 23-Jan-2020. Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( G e. ( Magma i^i ExId ) -> ran G = dom dom G )
Theorem	opidon2OLD 25443	Obsolete version of mndpfo 16061 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = ran G   =>    |- ( G e. ( Magma i^i ExId ) -> G : ( X X. X ) -onto-> X )
Theorem	isexid2 25444*	If G e. ( Magma i^i ExId ), then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = ran G   =>    |- ( G e. ( Magma i^i ExId ) -> E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )
Theorem	exidu1 25445*	Unicity of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = ran G   =>    |- ( G e. ( Magma i^i ExId ) -> E! u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )
Theorem	idrval 25446*	The value of the identity element. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = ran G   &    |- U = (GId ` G )   =>    |- ( G e. A -> U = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
Theorem	iorlid 25447	A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = ran G   &    |- U = (GId ` G )   =>    |- ( G e. ( Magma i^i ExId ) -> U e. X )
Theorem	cmpidelt 25448	A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = ran G   &    |- U = (GId ` G )   =>    |- ( ( G e. ( Magma i^i ExId ) /\ A e. X ) -> ( ( U G A ) = A /\ ( A G U ) = A ) )
Syntax	csem 25449	Extend class notation with the class of all semi-groups.
class SemiGrp
Definition	df-sgrOLD 25450	Obsolete version of df-sgrp 16028 as of 3-Feb-2020. A semi-group is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- SemiGrp = ( Magma i^i Ass )
Theorem	smgrpismgmOLD 25451	Obsolete version of sgrpmgm 16033 as of 3-Feb-2020. A semi-group is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( G e. SemiGrp -> G e. Magma )
Theorem	smgrpisass 25452	A semi-group is associative. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- ( G e. SemiGrp -> G e. Ass )
Theorem	issmgrpOLD 25453*	Obsolete version of issgrp 16029 as of 3-Feb-2020. The predicate "is a semi-group". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = dom dom G   =>    |- ( G e. A -> ( G e. SemiGrp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) ) )
Theorem	smgrpmgm 25454	A semi-group is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- X = dom dom G   =>    |- ( G e. SemiGrp -> G : ( X X. X ) --> X )
Theorem	smgrpassOLD 25455*	Obsolete version of sgrpass 16034 as of 3-Feb-2020. A semi-group is associative. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = dom dom G   =>    |- ( G e. SemiGrp -> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) )
Syntax	cmndo 25456	Extend class notation with the class of all monoids.
class MndOp
Definition	df-mndo 25457	A monoid is a semi-group with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- MndOp = ( SemiGrp i^i ExId )
Theorem	mndoissmgrpOLD 25458	Obsolete version of mndsgrp 16044 as of 3-Feb-2020. A monoid is a semi-group. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( G e. MndOp -> G e. SemiGrp )
Theorem	mndoisexid 25459	A monoid has an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- ( G e. MndOp -> G e. ExId )
Theorem	mndoismgmOLD 25460	Obsolete version of mndmgm 16045 as of 3-Feb-2020. A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( G e. MndOp -> G e. Magma )
Theorem	mndomgmid 25461	A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.)
|- ( G e. MndOp -> G e. ( Magma i^i ExId ) )
Theorem	ismndo 25462*	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = dom dom G   =>    |- ( G e. A -> ( G e. MndOp <-> ( G e. SemiGrp /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )
Theorem	ismndo1 25463*	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = dom dom G   =>    |- ( G e. A -> ( G e. MndOp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )
Theorem	ismndo2 25464*	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = ran G   =>    |- ( G e. A -> ( G e. MndOp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )
Theorem	grpomndo 25465	A group is a monoid. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- ( G e. GrpOp -> G e. MndOp )
18.1.6  Examples of Abelian groups
Theorem	ablosn 25466	Obsolete as of 23-Jan-2020. Use abl1 16989 instead. The Abelian group operation for the singleton group. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.)
|- A e. _V   =>    |- { <. <. A , A >. , A >. } e. AbelOp
Theorem	gidsn 25467	Obsolete as of 23-Jan-2020. Use mnd1id 16080 instead. The identity element of the trivial group. (Contributed by FL, 21-Jun-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
|- A e. _V   =>    |- (GId ` { <. <. A , A >. , A >. } ) = A
Theorem	ginvsn 25468	The inverse function of the trivial group. (Contributed by FL, 21-Jun-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
|- A e. _V   =>    |- ( inv ` { <. <. A , A >. , A >. } ) = ( _I |` { A } )
Theorem	cnaddablo 25469	Obsolete as of 23-Jan-2020. Use cnaddabl 16992 instead. Complex number addition is an Abelian group operation. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.)
|- + e. AbelOp
Theorem	cnid 25470	The group identity element of complex number addition is zero. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- 0 = (GId ` + )
Theorem	addinv 25471	Value of the group inverse of complex number addition. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- ( A e. CC -> ( ( inv ` + ) ` A ) = -u A )
Theorem	readdsubgo 25472	The real numbers under addition comprise a subgroup of the complex numbers under addition. (Contributed by Paul Chapman, 25-Apr-2008.) (New usage is discouraged.)
|- ( + |` ( RR X. RR ) ) e. ( SubGrpOp ` + )
Theorem	zaddsubgo 25473	The integers under addition comprise a subgroup of the complex numbers under addition. (Contributed by Paul Chapman, 25-Apr-2008.) (New usage is discouraged.)
|- ( + |` ( ZZ X. ZZ ) ) e. ( SubGrpOp ` + )
Theorem	ablomul 25474	Nonzero complex number multiplication is an Abelian group operation. (Contributed by Steve Rodriguez, 12-Feb-2007.) (New usage is discouraged.)
|- ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) e. AbelOp
Theorem	mulid 25475	The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007.) (Revised by Mario Carneiro, 17-Dec-2013.) (New usage is discouraged.)
|- (GId ` ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) ) = 1
18.1.7  Group homomorphism and isomorphism
Syntax	cghomOLD 25476	Obsolete version of cghm 16381 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.)
class GrpOpHom
Definition	df-ghomOLD 25477*	Obsolete version of df-ghm 16382 as of 15-Mar-2020. Define the set of group homomorphisms from g to h. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
|- GrpOpHom = ( g e. GrpOp , h e. GrpOp |-> { f | ( f : ran g --> ran h /\ A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) ) } )
Syntax	cgisoOLD 25478	Obsolete version of cgim 16422 as of 15-Mar-2020. Extend class notation to include the class of group isomorphisms. (New usage is discouraged.)
class GrpOpIso
Definition	df-gisoOLD 25479*	Obsolete version of df-gim 16424 as of 15-Mar-2020. Define the set of group isomorphisms from g to h. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
|- GrpOpIso = ( g e. GrpOp , h e. GrpOp |-> { f e. ( g GrpOpHom h ) | f : ran g -1-1-onto-> ran h } )
Theorem	elghomlem1OLD 25480*	Obsolete as of 15-Mar-2020. Lemma for elghomOLD 25482. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- S = { f | ( f : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) ) }   =>    |- ( ( G e. GrpOp /\ H e. GrpOp ) -> ( G GrpOpHom H ) = S )
Theorem	elghomlem2OLD 25481*	Obsolete as of 15-Mar-2020. Lemma for elghomOLD 25482. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- S = { f | ( f : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) ) }   =>    |- ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom H ) <-> ( F : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) ) )
Theorem	elghomOLD 25482*	Obsolete version of isghm 16384 as of 15-Mar-2020. Membership in the set of group homomorphisms from G to H. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = ran G   &    |- W = ran H   =>    |- ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom H ) <-> ( F : X --> W /\ A. x e. X A. y e. X ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) ) )
Theorem	ghomlinOLD 25483	Obsolete version of ghmlin 16389 as of 15-Mar-2020. Linearity of a group homomorphism. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = ran G   =>    |- ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) H ( F ` B ) ) = ( F ` ( A G B ) ) )
Theorem	ghomidOLD 25484	Obsolete version of ghmid 16390 as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- U = (GId ` G )   &    |- T = (GId ` H )   =>    |- ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F ` U ) = T )
Theorem	ghgrplem1OLD 25485*	Lemma for ghgrpOLD 25487. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> F : X -onto-> Y )   &    |- ( ( ph /\ w e. X ) -> ps )   &    |- ( C = ( F ` w ) -> ( ch <-> ps ) )   =>    |- ( ( ph /\ C e. Y ) -> ch )
Theorem	ghgrplem2OLD 25486*	Obsolete as of 14-Mar-2020. Lemma for ghgrpOLD 25487. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> F : X -onto-> Y )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x G y ) ) = ( ( F ` x ) O ( F ` y ) ) )   &    |- H = ( O |` ( Y X. Y ) )   =>    |- ( ( ph /\ ( C e. X /\ D e. X ) ) -> ( F ` ( C G D ) ) = ( ( F ` C ) H ( F ` D ) ) )
Theorem	ghgrpOLD 25487*	Obsolete version of ghmgrp 16311 as of 14-Mar-2020. The image of a group G under a group homomorphism F is a group. This is a stronger result than that usually found in the literature, since the target of the homomorphism (operator O in our model) need not have any of the properties of a group as a prerequisite. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> F : X -onto-> Y )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x G y ) ) = ( ( F ` x ) O ( F ` y ) ) )   &    |- H = ( O |` ( Y X. Y ) )   &    |- X = ran G   &    |- ( ph -> Y C_ A )   &    |- ( ph -> O Fn ( A X. A ) )   &    |- ( ph -> G e. GrpOp )   =>    |- ( ph -> H e. GrpOp )
Theorem	ghabloOLD 25488*	Obsolete version of ghmabl 16958 as of 14-Mar-2020. The image of an Abelian group G under a group homomorphism F is an Abelian group (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> F : X -onto-> Y )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x G y ) ) = ( ( F ` x ) O ( F ` y ) ) )   &    |- H = ( O |` ( Y X. Y ) )   &    |- X = ran G   &    |- ( ph -> Y C_ A )   &    |- ( ph -> O Fn ( A X. A ) )   &    |- ( ph -> G e. AbelOp )   =>    |- ( ph -> H e. AbelOp )
Theorem	ghsubgolemOLD 25489*	Obsolete as of 14-Mar-2020. The image of a subgroup S of group G under a group homomorphism F on G is a group, and furthermore is Abelian if S is Abelian. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> S e. ( SubGrpOp ` G ) )   &    |- X = ran G   &    |- ( ph -> F : X --> Y )   &    |- ( ph -> Y C_ A )   &    |- ( ph -> O Fn ( A X. A ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x G y ) ) = ( ( F ` x ) O ( F ` y ) ) )   &    |- Z = ran S   &    |- W = ( F " Z )   &    |- H = ( O |` ( W X. W ) )   =>    |- ( ph -> ( H e. GrpOp /\ ( S e. AbelOp -> H e. AbelOp ) ) )
Theorem	ghsubgoOLD 25490*	Obsolete version of ghmima 16404 as of 14-Mar-2020. The image of a subgroup S of group G under a group homomorphism F on G is a group. (Contributed by NM, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> S e. ( SubGrpOp ` G ) )   &    |- X = ran G   &    |- ( ph -> F : X --> Y )   &    |- ( ph -> Y C_ A )   &    |- ( ph -> O Fn ( A X. A ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x G y ) ) = ( ( F ` x ) O ( F ` y ) ) )   &    |- Z = ran S   &    |- W = ( F " Z )   &    |- H = ( O |` ( W X. W ) )   =>    |- ( ph -> H e. GrpOp )
Theorem	ghsubabloOLD 25491*	Obsolete version of ghmabl 16958 as of 5-Mar-2020. The image of an Abelian subgroup S of group G under a group homomorphism F on G is an Abelian group. (Contributed by Mario Carneiro, 12-May-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> S e. ( SubGrpOp ` G ) )   &    |- X = ran G   &    |- ( ph -> F : X --> Y )   &    |- ( ph -> Y C_ A )   &    |- ( ph -> O Fn ( A X. A ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x G y ) ) = ( ( F ` x ) O ( F ` y ) ) )   &    |- Z = ran S   &    |- W = ( F " Z )   &    |- H = ( O |` ( W X. W ) )   &    |- ( ph -> S e. AbelOp )   =>    |- ( ph -> H e. AbelOp )
Theorem	efghgrpOLD 25492*	Obsolete version of efabl 23022 as of 5-Mar-2020. The image of a subgroup of the group +, under the exponential function of a scaled complex number, is an Abelian group. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- S = { y | E. x e. X y = ( exp ` ( A x. x ) ) }   &    |- G = ( x. |` ( S X. S ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> X C_ CC )   &    |- ( + |` ( X X. X ) ) e. ( SubGrpOp ` + )   =>    |- ( ph -> G e. AbelOp )
Theorem	circgrpOLD 25493	Obsolete version of circgrp 23024 as of 5-Mar-2020. The circle group T is an Abelian group. (Contributed by Paul Chapman, 25-Mar-2008.) (Revised by Mario Carneiro, 13-May-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
|- C = ( `' abs " { 1 } )   &    |- T = ( x. |` ( C X. C ) )   =>    |- T e. AbelOp
18.2  Additional material on rings and fields
18.2.1  Definition and basic properties
Syntax	crngo 25494	Extend class notation with the class of all unital rings.
class RingOps
Definition	df-rngo 25495*	Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006.) (New usage is discouraged.)
|- RingOps = { <. g , h >. | ( ( g e. AbelOp /\ h : ( ran g X. ran g ) --> ran g ) /\ ( A. x e. ran g A. y e. ran g A. z e. ran g ( ( ( x h y ) h z ) = ( x h ( y h z ) ) /\ ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) /\ ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) ) /\ E. x e. ran g A. y e. ran g ( ( x h y ) = y /\ ( y h x ) = y ) ) ) }
Theorem	relrngo 25496	The class of all unital rings is a relation. (Contributed by FL, 31-Aug-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- Rel RingOps
Theorem	isrngo 25497*	The predicate "is a (unital) ring." Definition of ring with unit in [Schechter] p. 187. (Contributed by Jeff Hankins, 21-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- X = ran G   =>    |- ( H e. A -> ( <. G , H >. e. RingOps <-> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( A. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) )
Theorem	isrngod 25498*	Conditions that determine a ring. (Changed label from isringd 17346 to isrngod 25498-NM 2-Aug-2013.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- ( ph -> G e. AbelOp )   &    |- ( ph -> X = ran G )   &    |- ( ph -> H : ( X X. X ) --> X )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x H y ) H z ) = ( x H ( y H z ) ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) )   &    |- ( ph -> U e. X )   &    |- ( ( ph /\ y e. X ) -> ( U H y ) = y )   &    |- ( ( ph /\ y e. X ) -> ( y H U ) = y )   =>    |- ( ph -> <. G , H >. e. RingOps )
Theorem	rngoi 25499*	The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007.) (Proof shortened by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( R e. RingOps -> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( A. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) )
Theorem	rngosm 25500	Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( R e. RingOps -> H : ( X X. X ) --> X )