P. 128 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12701-12800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	submcl 12701	Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- .+ = ( +g ` M )   =>    |- ( ( S e. (SubMnd ` M ) /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )
Theorem	0subm 12702	The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.)
|- .0. = ( 0g ` G )   =>    |- ( G e. Mnd -> { .0. } e. (SubMnd ` G ) )
Theorem	insubm 12703	The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.)
|- ( ( A e. (SubMnd ` M ) /\ B e. (SubMnd ` M ) ) -> ( A i^i B ) e. (SubMnd ` M ) )
Theorem	0mhm 12704	The constant zero linear function between two monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- .0. = ( 0g ` N )   &    |- B = ( Base ` M )   =>    |- ( ( M e. Mnd /\ N e. Mnd ) -> ( B X. { .0. } ) e. ( M MndHom N ) )
Theorem	mhmco 12705	The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( F o. G ) e. ( S MndHom U ) )
Theorem	mhmima 12706	The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- ( ( F e. ( M MndHom N ) /\ X e. (SubMnd ` M ) ) -> ( F " X ) e. (SubMnd ` N ) )
Theorem	mhmeql 12707	The equalizer of two monoid homomorphisms is a submonoid. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> dom ( F i^i G ) e. (SubMnd ` S ) )
7.2  Groups
7.2.1  Definition and basic properties
Syntax	cgrp 12708	Extend class notation with class of all groups.
class Grp
Syntax	cminusg 12709	Extend class notation with inverse of group element.
class invg
Syntax	csg 12710	Extend class notation with group subtraction (or division) operation.
class -g
Definition	df-grp 12711*	Define class of all groups. A group is a monoid (df-mnd 12653) whose internal operation is such that every element admits a left inverse (which can be proven to be a two-sided inverse). Thus, a group G is an algebraic structure formed from a base set of elements (notated ( Base ` G ) per df-base 12422) and an internal group operation (notated ( +g ` G ) per df-plusg 12493). The operation combines any two elements of the group base set and must satisfy the 4 group axioms: closure (the result of the group operation must always be a member of the base set, see grpcl 12716), associativity (so ( ( a +g b ) +g c ) = ( a +g ( b +g c ) ) for any a, b, c, see grpass 12717), identity (there must be an element e = ( 0g ` G ) such that e +g a = a +g e = a for any a), and inverse (for each element a in the base set, there must be an element b = invg a in the base set such that a +g b = b +g a = e). It can be proven that the identity element is unique (grpideu 12719). Groups need not be commutative; a commutative group is an Abelian group. Subgroups can often be formed from groups. An example of an (Abelian) group is the set of complex numbers CC over the group operation + (addition). Other structures include groups, including unital rings and fields. (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
Definition	df-minusg 12712*	Define inverse of group element. (Contributed by NM, 24-Aug-2011.)
|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
Definition	df-sbg 12713*	Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014.)
|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
Theorem	isgrp 12714*	The predicate "is a group". (This theorem demonstrates the use of symbols as variable names, first proposed by FL in 2010.) (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Grp <-> ( G e. Mnd /\ A. a e. B E. m e. B ( m .+ a ) = .0. ) )
Theorem	grpmnd 12715	A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. Grp -> G e. Mnd )
Theorem	grpcl 12716	Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
Theorem	grpass 12717	A group operation is associative. (Contributed by NM, 14-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
Theorem	grpinvex 12718*	Every member of a group has a left inverse. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> E. y e. B ( y .+ X ) = .0. )
Theorem	grpideu 12719*	The two-sided identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 8-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> E! u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) )
Theorem	grpmndd 12720	A group is a monoid. (Contributed by SN, 1-Jun-2024.)
|- ( ph -> G e. Grp )   =>    |- ( ph -> G e. Mnd )
Theorem	grpcld 12721	Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .+ Y ) e. B )
Theorem	grpplusf 12722	The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- F = ( +f ` G )   =>    |- ( G e. Grp -> F : ( B X. B ) --> B )
Theorem	grpplusfo 12723	The group addition operation is a function onto the base set/set of group elements. (Contributed by NM, 30-Oct-2006.) (Revised by AV, 30-Aug-2021.)
|- B = ( Base ` G )   &    |- F = ( +f ` G )   =>    |- ( G e. Grp -> F : ( B X. B ) -onto-> B )
Theorem	grppropd 12724*	If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Oct-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. Grp <-> L e. Grp ) )
Theorem	grpprop 12725	If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by NM, 11-Oct-2013.)
|- ( Base ` K ) = ( Base ` L )   &    |- ( +g ` K ) = ( +g ` L )   =>    |- ( K e. Grp <-> L e. Grp )
Theorem	isgrpd2e 12726*	Deduce a group from its properties. In this version of isgrpd2 12727, we don't assume there is an expression for the inverse of x. (Contributed by NM, 10-Aug-2013.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> .0. = ( 0g ` G ) )   &    |- ( ph -> G e. Mnd )   &    |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = .0. )   =>    |- ( ph -> G e. Grp )
Theorem	isgrpd2 12727*	Deduce a group from its properties. N (negative) is normally dependent on x i.e. read it as N ( x ). Note: normally we don't use a ph antecedent on hypotheses that name structure components, since they can be eliminated with eqid 2170, but we make an exception for theorems such as isgrpd2 12727 and ismndd 12673 since theorems using them often rewrite the structure components. (Contributed by NM, 10-Aug-2013.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> .0. = ( 0g ` G ) )   &    |- ( ph -> G e. Mnd )   &    |- ( ( ph /\ x e. B ) -> N e. B )   &    |- ( ( ph /\ x e. B ) -> ( N .+ x ) = .0. )   =>    |- ( ph -> G e. Grp )
Theorem	isgrpde 12728*	Deduce a group from its properties. In this version of isgrpd 12729, we don't assume there is an expression for the inverse of x. (Contributed by NM, 6-Jan-2015.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> .0. e. B )   &    |- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )   &    |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = .0. )   =>    |- ( ph -> G e. Grp )
Theorem	isgrpd 12729*	Deduce a group from its properties. Unlike isgrpd2 12727, this one goes straight from the base properties rather than going through Mnd. N (negative) is normally dependent on x i.e. read it as N ( x ). (Contributed by NM, 6-Jun-2013.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> .0. e. B )   &    |- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )   &    |- ( ( ph /\ x e. B ) -> N e. B )   &    |- ( ( ph /\ x e. B ) -> ( N .+ x ) = .0. )   =>    |- ( ph -> G e. Grp )
Theorem	isgrpi 12730*	Properties that determine a group. N (negative) is normally dependent on x i.e. read it as N ( x ). (Contributed by NM, 3-Sep-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ( x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- .0. e. B   &    |- ( x e. B -> ( .0. .+ x ) = x )   &    |- ( x e. B -> N e. B )   &    |- ( x e. B -> ( N .+ x ) = .0. )   =>    |- G e. Grp
Theorem	grpsgrp 12731	A group is a semigroup. (Contributed by AV, 28-Aug-2021.)
|- ( G e. Grp -> G e. Smgrp )
Theorem	dfgrp2 12732*	Alternate definition of a group as semigroup with a left identity and a left inverse for each element. This "definition" is weaker than df-grp 12711, based on the definition of a monoid which provides a left and a right identity. (Contributed by AV, 28-Aug-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Grp <-> ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) )
Theorem	dfgrp2e 12733*	Alternate definition of a group as a set with a closed, associative operation, a left identity and a left inverse for each element. Alternate definition in [Lang] p. 7. (Contributed by NM, 10-Oct-2006.) (Revised by AV, 28-Aug-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Grp <-> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) )
Theorem	grpidcl 12734	The identity element of a group belongs to the group. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> .0. e. B )
Theorem	grpbn0 12735	The base set of a group is not empty. It is also inhabited (see grpidcl 12734). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- B = ( Base ` G )   =>    |- ( G e. Grp -> B =/= (/) )
Theorem	grplid 12736	The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( .0. .+ X ) = X )
Theorem	grprid 12737	The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( X .+ .0. ) = X )
Theorem	grpn0 12738	A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- ( G e. Grp -> G =/= (/) )
Theorem	hashfingrpnn 12739	A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> (♯ ` B ) e. NN )
Theorem	grprcan 12740	Right cancellation law for groups. (Contributed by NM, 24-Aug-2011.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Z ) = ( Y .+ Z ) <-> X = Y ) )
Theorem	grpinveu 12741*	The left inverse element of a group is unique. Lemma 2.2.1(b) of [Herstein] p. 55. (Contributed by NM, 24-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> E! y e. B ( y .+ X ) = .0. )
Theorem	grpid 12742	Two ways of saying that an element of a group is the identity element. Provides a convenient way to compute the value of the identity element. (Contributed by NM, 24-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( ( X .+ X ) = X <-> .0. = X ) )
Theorem	isgrpid2 12743	Properties showing that an element Z is the identity element of a group. (Contributed by NM, 7-Aug-2013.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> ( ( Z e. B /\ ( Z .+ Z ) = Z ) <-> .0. = Z ) )
Theorem	grpidd2 12744*	Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 12729. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> .0. e. B )   &    |- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )   &    |- ( ph -> G e. Grp )   =>    |- ( ph -> .0. = ( 0g ` G ) )
Theorem	grpinvfvalg 12745*	The inverse function of a group. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) (Revised by Rohan Ridenour, 13-Aug-2023.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( G e. V -> N = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) )
Theorem	grpinvval 12746*	The inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( X e. B -> ( N ` X ) = ( iota_ y e. B ( y .+ X ) = .0. ) )
Theorem	grpinvfng 12747	Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   =>    |- ( G e. V -> N Fn B )
Theorem	grpsubfvalg 12748*	Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-Feb-2024.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- I = ( invg ` G )   &    |- .- = ( -g ` G )   =>    |- ( G e. V -> .- = ( x e. B , y e. B |-> ( x .+ ( I ` y ) ) ) )
Theorem	grpsubval 12749	Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- I = ( invg ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( I ` Y ) ) )
Theorem	grpinvf 12750	The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   =>    |- ( G e. Grp -> N : B --> B )
Theorem	grpinvcl 12751	A group element's inverse is a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )
Theorem	grplinv 12752	The left inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) .+ X ) = .0. )
Theorem	grprinv 12753	The right inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( X .+ ( N ` X ) ) = .0. )
Theorem	grpinvid1 12754	The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( N ` X ) = Y <-> ( X .+ Y ) = .0. ) )
Theorem	grpinvid2 12755	The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( N ` X ) = Y <-> ( Y .+ X ) = .0. ) )
Theorem	isgrpinv 12756*	Properties showing that a function M is the inverse function of a group. (Contributed by NM, 7-Aug-2013.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( G e. Grp -> ( ( M : B --> B /\ A. x e. B ( ( M ` x ) .+ x ) = .0. ) <-> N = M ) )
Theorem	grplrinv 12757*	In a group, every member has a left and right inverse. (Contributed by AV, 1-Sep-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> A. x e. B E. y e. B ( ( y .+ x ) = .0. /\ ( x .+ y ) = .0. ) )
Theorem	grpidinv2 12758*	A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010.) (Revised by AV, 1-Sep-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ A e. B ) -> ( ( ( .0. .+ A ) = A /\ ( A .+ .0. ) = A ) /\ E. y e. B ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) ) )
Theorem	grpidinv 12759*	A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006.) (Revised by AV, 1-Sep-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Grp -> E. u e. B A. x e. B ( ( ( u .+ x ) = x /\ ( x .+ u ) = x ) /\ E. y e. B ( ( y .+ x ) = u /\ ( x .+ y ) = u ) ) )
Theorem	grpinvid 12760	The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.)
|- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( G e. Grp -> ( N ` .0. ) = .0. )
Theorem	grplcan 12761	Left cancellation law for groups. (Contributed by NM, 25-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Z .+ X ) = ( Z .+ Y ) <-> X = Y ) )
Theorem	grpasscan1 12762	An associative cancellation law for groups. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by AV, 30-Aug-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ ( ( N ` X ) .+ Y ) ) = Y )
Theorem	grpasscan2 12763	An associative cancellation law for groups. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .+ ( N ` Y ) ) .+ Y ) = X )
Theorem	grpidrcan 12764	If right adding an element of a group to an arbitrary element of the group results in this element, the added element is the identity element and vice versa. (Contributed by AV, 15-Mar-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( ( X .+ Z ) = X <-> Z = .0. ) )
Theorem	grpidlcan 12765	If left adding an element of a group to an arbitrary element of the group results in this element, the added element is the identity element and vice versa. (Contributed by AV, 15-Mar-2019.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( ( Z .+ X ) = X <-> Z = .0. ) )
Theorem	grpinvinv 12766	Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B ) -> ( N ` ( N ` X ) ) = X )
Theorem	grpinvcnv 12767	The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   =>    |- ( G e. Grp -> `' N = N )
Theorem	grpinv11 12768	The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) = ( N ` Y ) <-> X = Y ) )
Theorem	grpinvf1o 12769	The group inverse is a one-to-one onto function. (Contributed by NM, 22-Oct-2014.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- N = ( invg ` G )   &    |- ( ph -> G e. Grp )   =>    |- ( ph -> N : B -1-1-onto-> B )
Theorem	grpinvnz 12770	The inverse of a nonzero group element is not zero. (Contributed by Stefan O'Rear, 27-Feb-2015.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. B /\ X =/= .0. ) -> ( N ` X ) =/= .0. )
Theorem	grpinvnzcl 12771	The inverse of a nonzero group element is a nonzero group element. (Contributed by Stefan O'Rear, 27-Feb-2015.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- N = ( invg ` G )   =>    |- ( ( G e. Grp /\ X e. ( B \ { .0. } ) ) -> ( N ` X ) e. ( B \ { .0. } ) )
Theorem	grpsubinv 12772	Subtraction of an inverse. (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- N = ( invg ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .- ( N ` Y ) ) = ( X .+ Y ) )
7.3  The complex numbers as an algebraic extensible structure
7.3.1  Definition and basic properties
Syntax	cpsmet 12773	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmet 12774	Extend class notation with the class of all extended metric spaces.
class *Met
Syntax	cmet 12775	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 12776	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 12777	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 12778	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 12779	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 12780	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 12781*	Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- PsMet = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x ( ( y d y ) = 0 /\ A. z e. x A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )
Definition	df-xmet 12782*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 12783, but we also allow the metric to take on the value +oo. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- *Met = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )
Definition	df-met 12783*	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. (Contributed by NM, 25-Aug-2006.)
|- Met = ( x e. _V |-> { d e. ( RR ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) ) } )
Definition	df-bl 12784*	Define the metric space ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
Definition	df-mopn 12785	Define a function whose value is the family of open sets of a metric space. (Contributed by NM, 1-Sep-2006.)
|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
Definition	df-fbas 12786*	Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
|- fBas = ( w e. _V |-> { x e. ~P ~P w | ( x =/= (/) /\ (/) e/ x /\ A. y e. x A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/) ) } )
Definition	df-fg 12787*	Define the filter generating function. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
Definition	df-metu 12788*	Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
PART 8  BASIC TOPOLOGY
8.1  Topology
8.1.1  Topological spaces A topology on a set is a set of subsets of that set, called open sets, which satisfy certain conditions. One condition is that the whole set be an open set. Therefore, a set is recoverable from a topology on it (as its union), and it may sometimes be more convenient to consider topologies without reference to the underlying set.
8.1.1.1  Topologies
Syntax	ctop 12789	Syntax for the class of topologies.
class Top
Definition	df-top 12790*	Define the class of topologies. It is a proper class. See istopg 12791 and istopfin 12792 for the corresponding characterizations, using respectively binary intersections like in this definition and nonempty finite intersections. The final form of the definition is due to Bourbaki (Def. 1 of [BourbakiTop1] p. I.1), while the idea of defining a topology in terms of its open sets is due to Aleksandrov. For the convoluted history of the definitions of these notions, see Gregory H. Moore, The emergence of open sets, closed sets, and limit points in analysis and topology, Historia Mathematica 35 (2008) 220--241. (Contributed by NM, 3-Mar-2006.) (Revised by BJ, 20-Oct-2018.)
|- Top = { x | ( A. y e. ~P x U. y e. x /\ A. y e. x A. z e. x ( y i^i z ) e. x ) }
Theorem	istopg 12791*	Express the predicate " J is a topology". See istopfin 12792 for another characterization using nonempty finite intersections instead of binary intersections. Note: In the literature, a topology is often represented by a calligraphic letter T, which resembles the letter J. This confusion may have led to J being used by some authors (e.g., K. D. Joshi, Introduction to General Topology (1983), p. 114) and it is convenient for us since we later use T to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- ( J e. A -> ( J e. Top <-> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) )
Theorem	istopfin 12792*	Express the predicate " J is a topology" using nonempty finite intersections instead of binary intersections as in istopg 12791. It is not clear we can prove the converse without adding additional conditions. (Contributed by NM, 19-Jul-2006.) (Revised by Jim Kingdon, 14-Jan-2023.)
|- ( J e. Top -> ( A. x ( x C_ J -> U. x e. J ) /\ A. x ( ( x C_ J /\ x =/= (/) /\ x e. Fin ) -> |^| x e. J ) ) )
Theorem	uniopn 12793	The union of a subset of a topology (that is, the union of any family of open sets of a topology) is an open set. (Contributed by Stefan Allan, 27-Feb-2006.)
|- ( ( J e. Top /\ A C_ J ) -> U. A e. J )
Theorem	iunopn 12794*	The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.)
|- ( ( J e. Top /\ A. x e. A B e. J ) -> U_ x e. A B e. J )
Theorem	inopn 12795	The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )
Theorem	fiinopn 12796	The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.)
|- ( J e. Top -> ( ( A C_ J /\ A =/= (/) /\ A e. Fin ) -> |^| A e. J ) )
Theorem	unopn 12797	The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A u. B ) e. J )
Theorem	0opn 12798	The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.)
|- ( J e. Top -> (/) e. J )
Theorem	0ntop 12799	The empty set is not a topology. (Contributed by FL, 1-Jun-2008.)
|- -. (/) e. Top
Theorem	topopn 12800	The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
|- X = U. J   =>    |- ( J e. Top -> X e. J )