P. 151 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 15001-15100   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-gim 15001*	An isomorphism of groups is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group operation. (Contributed by Stefan O'Rear, 21-Jan-2015.)
|- GrpIso = ( s e. Grp , t e. Grp |-> { g e. ( s GrpHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )
Definition	df-gic 15002	Two groups are said to be isomorphic iff they are connected by at least one isomorphism. Isomophic groups share all global group properties, but to relate local properties requires knowledge of a specific isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ~=ph𝑔 = ( `' GrpIso " ( _V \ 1o ) )
Theorem	gimfn 15003	The group isomorphism function is a well-defined function. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- GrpIso Fn ( Grp X. Grp )
Theorem	isgim 15004	An isomorphism of groups is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R GrpIso S ) <-> ( F e. ( R GrpHom S ) /\ F : B -1-1-onto-> C ) )
Theorem	gimf1o 15005	An isomorphism of groups is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R GrpIso S ) -> F : B -1-1-onto-> C )
Theorem	gimghm 15006	An isomorphism of groups is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( F e. ( R GrpIso S ) -> F e. ( R GrpHom S ) )
Theorem	isgim2 15007	A group isomorphism is a homomorphism whose converse is also a homomorphism. Characterization of isomorphisms similar to ishmeo 17744. (Contributed by Mario Carneiro, 6-May-2015.)
|- ( F e. ( R GrpIso S ) <-> ( F e. ( R GrpHom S ) /\ `' F e. ( S GrpHom R ) ) )
Theorem	subggim 15008	Behavior of subgroups under isomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.)
|- B = ( Base ` R )   =>    |- ( ( F e. ( R GrpIso S ) /\ A C_ B ) -> ( A e. (SubGrp ` R ) <-> ( F " A ) e. (SubGrp ` S ) ) )
Theorem	gimcnv 15009	The converse of a bijective group homomorphism is a bijective group homomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( F e. ( S GrpIso T ) -> `' F e. ( T GrpIso S ) )
Theorem	gimco 15010	The composition of group isomorphisms is a group isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- ( ( F e. ( T GrpIso U ) /\ G e. ( S GrpIso T ) ) -> ( F o. G ) e. ( S GrpIso U ) )
Theorem	brgic 15011	The relation "is isomorphic to" for groups. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( R ~=ph𝑔 S <-> ( R GrpIso S ) =/= (/) )
Theorem	brgici 15012	Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( F e. ( R GrpIso S ) -> R ~=ph𝑔 S )
Theorem	gicref 15013	Isomorphism is reflexive. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- ( R e. Grp -> R ~=ph𝑔 R )
Theorem	giclcl 15014	Isomorphism implies the left side is a group. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( R ~=ph𝑔 S -> R e. Grp )
Theorem	gicrcl 15015	Isomorphism implies the right side is a group. (Contributed by Mario Carneiro, 6-May-2015.)
|- ( R ~=ph𝑔 S -> S e. Grp )
Theorem	gicsym 15016	Isomorphism is symmetric. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- ( R ~=ph𝑔 S -> S ~=ph𝑔 R )
Theorem	gictr 15017	Isomorphism is transitive. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- ( ( R ~=ph𝑔 S /\ S ~=ph𝑔 T ) -> R ~=ph𝑔 T )
Theorem	gicer 15018	Isomorphism is an equivalence relation on groups. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- ~=ph𝑔 Er Grp
Theorem	gicen 15019	Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( R ~=ph𝑔 S -> B ~~ C )
Theorem	gicsubgen 15020	A less trivial example of a group invariant: cardinality of the subgroup lattice. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( R ~=ph𝑔 S -> (SubGrp ` R ) ~~ (SubGrp ` S ) )
10.2.5  Group actions
Syntax	cga 15021	Extend class definition to include the class of group actions.
class GrpAct
Definition	df-ga 15022*	Define the class of all group actions. A group G acts on a set S if a permutation on S is associated with every element of G in such a way that the identity permutation on S is associated with the neutral element of G, and the composition of the permutations associated with two elements of G is identical with the permutation associated to the composition of these two elements (in the same order) in the group G. (Contributed by Jeff Hankins, 10-Aug-2009.)
|- GrpAct = ( g e. Grp , s e. _V |-> [_ ( Base ` g ) / b ]_ { m e. ( s ^m ( b X. s ) ) | A. x e. s ( ( ( 0g ` g ) m x ) = x /\ A. y e. b A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) ) ) } )
Theorem	isga 15023*	The predicate "is a (left) group action." The group G is said to act on the base set Y of the action, which is not assumed to have any special properties. There is a related notion of right group action, but as the Wikipedia article explains, it is not mathematically interesting. The way actions are usually thought of is that each element g of G is a permutation of the elements of Y (see gapm 15038). Since group theory was classically about symmetry groups, it is therefore likely that the notion of group action was useful even in early group theory. (Contributed by Jeff Hankins, 10-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( .(+) e. ( G GrpAct Y ) <-> ( ( G e. Grp /\ Y e. _V ) /\ ( .(+) : ( X X. Y ) --> Y /\ A. x e. Y ( ( .0. .(+) x ) = x /\ A. y e. X A. z e. X ( ( y .+ z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) ) ) )
Theorem	gagrp 15024	The left argument of a group action is a group. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- ( .(+) e. ( G GrpAct Y ) -> G e. Grp )
Theorem	gaset 15025	The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- ( .(+) e. ( G GrpAct Y ) -> Y e. _V )
Theorem	gagrpid 15026	The identity of the group does not alter the base set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- .0. = ( 0g ` G )   =>    |- ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ( .0. .(+) A ) = A )
Theorem	gaf 15027	The mapping of the group action operation. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   =>    |- ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) --> Y )
Theorem	gafo 15028	A group action is onto its base set. (Contributed by Jeff Hankins, 10-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   =>    |- ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) -onto-> Y )
Theorem	gaass 15029	An "associative" property for group actions. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. X /\ C e. Y ) ) -> ( ( A .+ B ) .(+) C ) = ( A .(+) ( B .(+) C ) ) )
Theorem	ga0 15030	The action of a group on the empty set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- ( G e. Grp -> (/) e. ( G GrpAct (/) ) )
Theorem	gaid 15031	The trivial action of a group on any set. Each group element corresponds to the identity permutation. (Contributed by Jeff Hankins, 11-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   =>    |- ( ( G e. Grp /\ S e. V ) -> ( 2nd |` ( X X. S ) ) e. ( G GrpAct S ) )
Theorem	subgga 15032*	A subgroup acts on its parent group. (Contributed by Jeff Hankins, 13-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- H = ( G ↾s Y )   &    |- F = ( x e. Y , y e. X |-> ( x .+ y ) )   =>    |- ( Y e. (SubGrp ` G ) -> F e. ( H GrpAct X ) )
Theorem	gass 15033*	A subset of a group action is a group action iff it is closed under the group action operation. (Contributed by Mario Carneiro, 17-Jan-2015.)
|- X = ( Base ` G )   =>    |- ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) -> ( ( .(+) |` ( X X. Z ) ) e. ( G GrpAct Z ) <-> A. x e. X A. y e. Z ( x .(+) y ) e. Z ) )
Theorem	gasubg 15034	The restriction of a group action to a subgroup is a group action. (Contributed by Mario Carneiro, 17-Jan-2015.)
|- H = ( G ↾s S )   =>    |- ( ( .(+) e. ( G GrpAct Y ) /\ S e. (SubGrp ` G ) ) -> ( .(+) |` ( S X. Y ) ) e. ( H GrpAct Y ) )
Theorem	gaid2 15035*	A group operation is a left group action of the group on itself. (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- F = ( x e. X , y e. X |-> ( x .+ y ) )   =>    |- ( G e. Grp -> F e. ( G GrpAct X ) )
Theorem	galcan 15036	The action of a particular group element is left-cancelable. (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   =>    |- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A .(+) B ) = ( A .(+) C ) <-> B = C ) )
Theorem	gacan 15037	Group inverses cancel in a group action. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- N = ( inv g ` G )   =>    |- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A .(+) B ) = C <-> ( ( N ` A ) .(+) C ) = B ) )
Theorem	gapm 15038*	The action of a particular group element is a permutation of the base set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- F = ( x e. Y |-> ( A .(+) x ) )   =>    |- ( ( .(+) e. ( G GrpAct Y ) /\ A e. X ) -> F : Y -1-1-onto-> Y )
Theorem	gaorb 15039*	The orbit equivalence relation puts two points in the group action in the same equivalence class iff there is a group element that takes one element to the other. (Contributed by Mario Carneiro, 14-Jan-2015.)
|- .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }   =>    |- ( A .~ B <-> ( A e. Y /\ B e. Y /\ E. h e. X ( h .(+) A ) = B ) )
Theorem	gaorber 15040*	The orbit equivalence relation is an equivalence relation on the target set of the group action. (Contributed by NM, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }   &    |- X = ( Base ` G )   =>    |- ( .(+) e. ( G GrpAct Y ) -> .~ Er Y )
Theorem	gastacl 15041*	The stabilizer subgroup in a group action. (Contributed by Mario Carneiro, 15-Jan-2015.)
|- X = ( Base ` G )   &    |- H = { u e. X | ( u .(+) A ) = A }   =>    |- ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> H e. (SubGrp ` G ) )
Theorem	gastacos 15042*	Write the coset relation for the stabilizer subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.)
|- X = ( Base ` G )   &    |- H = { u e. X | ( u .(+) A ) = A }   &    |- .~ = ( G ~QG H )   =>    |- ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( B .~ C <-> ( B .(+) A ) = ( C .(+) A ) ) )
Theorem	orbstafun 15043*	Existence and uniqueness for the function of orbsta 15045. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- X = ( Base ` G )   &    |- H = { u e. X | ( u .(+) A ) = A }   &    |- .~ = ( G ~QG H )   &    |- F = ran ( k e. X |-> <. [ k ] .~ , ( k .(+) A ) >. )   =>    |- ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> Fun F )
Theorem	orbstaval 15044*	Value of the function at a given equivalence class element. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- X = ( Base ` G )   &    |- H = { u e. X | ( u .(+) A ) = A }   &    |- .~ = ( G ~QG H )   &    |- F = ran ( k e. X |-> <. [ k ] .~ , ( k .(+) A ) >. )   =>    |- ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ B e. X ) -> ( F ` [ B ] .~ ) = ( B .(+) A ) )
Theorem	orbsta 15045*	The Orbit-Stabilizer theorem. The mapping F is a bijection from the cosets of the stabilizer subgroup of A to the orbit of A. (Contributed by Mario Carneiro, 15-Jan-2015.)
|- X = ( Base ` G )   &    |- H = { u e. X | ( u .(+) A ) = A }   &    |- .~ = ( G ~QG H )   &    |- F = ran ( k e. X |-> <. [ k ] .~ , ( k .(+) A ) >. )   &    |- O = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }   =>    |- ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> F : ( X /. .~ ) -1-1-onto-> [ A ] O )
Theorem	orbsta2 15046*	Relation between the size of the orbit and the size of the stabilizer of a point in a finite group action. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- X = ( Base ` G )   &    |- H = { u e. X | ( u .(+) A ) = A }   &    |- .~ = ( G ~QG H )   &    |- O = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }   =>    |- ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> ( # ` X ) = ( ( # ` [ A ] O ) x. ( # ` H ) ) )
10.2.6  Symmetry groups and Cayley's Theorem
Syntax	csymg 15047	Extend class notation to include the class of symmetry groups.
class SymGrp
Definition	df-symg 15048*	Define the symmetry group on set x. We represent the group as the set of 1-1-onto functions from x to itself under function composition, and topologize it as a function space assuming the set is discrete. (Contributed by Paul Chapman, 25-Feb-2008.)
|- SymGrp = ( x e. _V |-> [_ { h | h : x -1-1-onto-> x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( x X. { ~P x } ) ) >. } )
Theorem	symgval 15049*	The value of the symmetry group function at A. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 12-Jan-2015.)
|- G = ( SymGrp ` A )   &    |- B = { x | x : A -1-1-onto-> A }   &    |- .+ = ( f e. B , g e. B |-> ( f o. g ) )   &    |- J = ( Xt_ ` ( A X. { ~P A } ) )   =>    |- ( A e. V -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. } )
Theorem	symgbas 15050*	The base set of the symmetric group. (Contributed by Mario Carneiro, 12-Jan-2015.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   =>    |- B = { x | x : A -1-1-onto-> A }
Theorem	elsymgbas2 15051	Two ways of saying a function is a 1-1-onto mapping of A to itself. (Contributed by Mario Carneiro, 28-Jan-2015.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   =>    |- ( F e. V -> ( F e. B <-> F : A -1-1-onto-> A ) )
Theorem	elsymgbas 15052	Two ways of saying a function is a 1-1-onto mapping of A to itself. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 28-Jan-2015.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   =>    |- ( A e. V -> ( F e. B <-> F : A -1-1-onto-> A ) )
Theorem	symghash 15053	The symmetric group on n objects has cardinality n !. (Contributed by Mario Carneiro, 22-Jan-2015.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   =>    |- ( A e. Fin -> ( # ` B ) = ( ! ` ( # ` A ) ) )
Theorem	symgplusg 15054*	The value of the symmetry group function at A. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 28-Jan-2015.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- .+ = ( f e. B , g e. B |-> ( f o. g ) )
Theorem	symgov 15055	The value of the group operation of the symmetry group on A. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 28-Jan-2015.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) )
Theorem	symgcl 15056	The group operation of the symmetry group on A is closed, i.e. a magma. (Contributed by Mario Carneiro, 12-Jan-2015.) (Revised by Mario Carneiro, 28-Jan-2015.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
Theorem	symgtset 15057	The topology of the symmetry group on A. This component is defined on a larger set than the true base - the product topology is defined on the set of all functions, not just bijections - but the definition of TopOpen ensures that it is trimmed down before it gets use. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- G = ( SymGrp ` A )   =>    |- ( A e. V -> ( Xt_ ` ( A X. { ~P A } ) ) = (TopSet ` G ) )
Theorem	symggrp 15058	The symmetry group on A is a group. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- G = ( SymGrp ` A )   =>    |- ( A e. V -> G e. Grp )
Theorem	symgid 15059	The value of the identity element of the symmetry group on A (Contributed by Paul Chapman, 25-Jul-2008.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- G = ( SymGrp ` A )   =>    |- ( A e. V -> ( _I |` A ) = ( 0g ` G ) )
Theorem	symginv 15060	The group inverse in the symmetric group corresponds to the functional inverse. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by Mario Carneiro, 2-Sep-2015.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   &    |- N = ( inv g ` G )   =>    |- ( F e. B -> ( N ` F ) = `' F )
Theorem	galactghm 15061*	The currying of a group action is a group homomorphism between the group G and the symetry group ( SymGrp ` Y ). (Contributed by FL, 17-May-2010.) (Proof shortened by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- H = ( SymGrp ` Y )   &    |- F = ( x e. X |-> ( y e. Y |-> ( x .(+) y ) ) )   =>    |- ( .(+) e. ( G GrpAct Y ) -> F e. ( G GrpHom H ) )
Theorem	lactghmga 15062*	The converse of galactghm 15061. The uncurrying of a homomorphism into ( SymGrp ` Y ) is a group action. Thus, group actions and group homomorphisms into a symmetric group are essentially equivalent notions. (Contributed by Mario Carneiro, 15-Jan-2015.)
|- X = ( Base ` G )   &    |- H = ( SymGrp ` Y )   &    |- .(+) = ( x e. X , y e. Y |-> ( ( F ` x ) ` y ) )   =>    |- ( F e. ( G GrpHom H ) -> .(+) e. ( G GrpAct Y ) )
Theorem	symgtopn 15063	The topology of the symmetry group on A. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- G = ( SymGrp ` X )   &    |- B = ( Base ` G )   =>    |- ( X e. V -> ( ( Xt_ ` ( X X. { ~P X } ) ) ↾t B ) = ( TopOpen ` G ) )
Theorem	symgga 15064*	The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- G = ( SymGrp ` X )   &    |- B = ( Base ` G )   &    |- F = ( f e. B , x e. X |-> ( f ` x ) )   =>    |- ( X e. V -> F e. ( G GrpAct X ) )
Theorem	cayleylem1 15065*	Lemma for cayley 15067. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- H = ( SymGrp ` X )   &    |- S = ( Base ` H )   &    |- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )   =>    |- ( G e. Grp -> F e. ( G GrpHom H ) )
Theorem	cayleylem2 15066*	Lemma for cayley 15067. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- H = ( SymGrp ` X )   &    |- S = ( Base ` H )   &    |- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )   =>    |- ( G e. Grp -> F : X -1-1-> S )
Theorem	cayley 15067*	Cayley's Theorem (constructive version): given group G, F is an isomorphism between G and the subgroup S of the symmetry group H on the underlying set X of G. (Contributed by Paul Chapman, 3-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- H = ( SymGrp ` X )   &    |- .+ = ( +g ` G )   &    |- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )   &    |- S = ran F   =>    |- ( G e. Grp -> ( S e. (SubGrp ` H ) /\ F e. ( G GrpHom ( H ↾s S ) ) /\ F : X -1-1-onto-> S ) )
Theorem	cayleyth 15068*	Cayley's Theorem (existence version): every group G is isomorphic to a subgroup of the symmetry group on the underlying set of G. (For any group G there exists an isomorphism f between G and a subgroup h of the symmetry group on the underlying set of G.) (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.)
|- X = ( Base ` G )   &    |- H = ( SymGrp ` X )   =>    |- ( G e. Grp -> E. s e. (SubGrp ` H ) E. f e. ( G GrpHom ( H ↾s s ) ) f : X -1-1-onto-> s )
10.2.7  Centralizers and centers
Syntax	ccntz 15069	Syntax for the centralizer of a set in a monoid.
class Cntz
Syntax	ccntr 15070	Syntax for the centralizer of a monoid.
class Cntr
Definition	df-cntz 15071*	Define the centralizer of a subset of a magma, which is the set of elements each of which commutes with each element of the given subset. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- Cntz = ( m e. _V |-> ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } ) )
Definition	df-cntr 15072	Define the center of a magma, which is the elements that commute with all others. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- Cntr = ( m e. _V |-> ( (Cntz ` m ) ` ( Base ` m ) ) )
Theorem	cntrval 15073	Substitute definition of the center. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- B = ( Base ` M )   &    |- Z = (Cntz ` M )   =>    |- ( Z ` B ) = (Cntr ` M )
Theorem	cntzfval 15074*	First level substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   &    |- Z = (Cntz ` M )   =>    |- ( M e. V -> Z = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) )
Theorem	cntzval 15075*	Definition substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   &    |- Z = (Cntz ` M )   =>    |- ( S C_ B -> ( Z ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } )
Theorem	elcntz 15076*	Elementhood in the centralizer. (Contributed by Mario Carneiro, 22-Sep-2015.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   &    |- Z = (Cntz ` M )   =>    |- ( S C_ B -> ( A e. ( Z ` S ) <-> ( A e. B /\ A. y e. S ( A .+ y ) = ( y .+ A ) ) ) )
Theorem	cntzel 15077*	Membership in a centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   &    |- Z = (Cntz ` M )   =>    |- ( ( S C_ B /\ X e. B ) -> ( X e. ( Z ` S ) <-> A. y e. S ( X .+ y ) = ( y .+ X ) ) )
Theorem	cntzsnval 15078*	Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   &    |- Z = (Cntz ` M )   =>    |- ( Y e. B -> ( Z ` { Y } ) = { x e. B | ( x .+ Y ) = ( Y .+ x ) } )
Theorem	elcntzsn 15079	Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   &    |- Z = (Cntz ` M )   =>    |- ( Y e. B -> ( X e. ( Z ` { Y } ) <-> ( X e. B /\ ( X .+ Y ) = ( Y .+ X ) ) ) )
Theorem	sscntz 15080*	A centralizer expression for two sets elementwise commuting. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   &    |- Z = (Cntz ` M )   =>    |- ( ( S C_ B /\ T C_ B ) -> ( S C_ ( Z ` T ) <-> A. x e. S A. y e. T ( x .+ y ) = ( y .+ x ) ) )
Theorem	cntzrcl 15081	Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- B = ( Base ` M )   &    |- Z = (Cntz ` M )   =>    |- ( X e. ( Z ` S ) -> ( M e. _V /\ S C_ B ) )
Theorem	cntzssv 15082	The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- B = ( Base ` M )   &    |- Z = (Cntz ` M )   =>    |- ( Z ` S ) C_ B
Theorem	cntzi 15083	Membership in a centralizer (inference). (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- .+ = ( +g ` M )   &    |- Z = (Cntz ` M )   =>    |- ( ( X e. ( Z ` S ) /\ Y e. S ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	cntri 15084	Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   &    |- Z = (Cntr ` M )   =>    |- ( ( X e. Z /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	resscntz 15085	Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015.)
|- H = ( G ↾s A )   &    |- Z = (Cntz ` G )   &    |- Y = (Cntz ` H )   =>    |- ( ( A e. V /\ S C_ A ) -> ( Y ` S ) = ( ( Z ` S ) i^i A ) )
Theorem	cntz2ss 15086	Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015.)
|- B = ( Base ` M )   &    |- Z = (Cntz ` M )   =>    |- ( ( S C_ B /\ T C_ S ) -> ( Z ` S ) C_ ( Z ` T ) )
Theorem	cntzrec 15087	Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- B = ( Base ` M )   &    |- Z = (Cntz ` M )   =>    |- ( ( S C_ B /\ T C_ B ) -> ( S C_ ( Z ` T ) <-> T C_ ( Z ` S ) ) )
Theorem	cntziinsn 15088*	Express any centralizer as an intersection of singleton centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- B = ( Base ` M )   &    |- Z = (Cntz ` M )   =>    |- ( S C_ B -> ( Z ` S ) = ( B i^i |^|_ x e. S ( Z ` { x } ) ) )
Theorem	cntzsubm 15089	Centralizers in a monoid are submonoids. (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` M )   &    |- Z = (Cntz ` M )   =>    |- ( ( M e. Mnd /\ S C_ B ) -> ( Z ` S ) e. (SubMnd ` M ) )
Theorem	cntzsubg 15090	Centralizers in a group are subgroups. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- B = ( Base ` M )   &    |- Z = (Cntz ` M )   =>    |- ( ( M e. Grp /\ S C_ B ) -> ( Z ` S ) e. (SubGrp ` M ) )
Theorem	cntzidss 15091	If the elements of S commute, the elements of a subset T also commute. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- Z = (Cntz ` G )   =>    |- ( ( S C_ ( Z ` S ) /\ T C_ S ) -> T C_ ( Z ` T ) )
Theorem	cntzmhm 15092	Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- Z = (Cntz ` G )   &    |- Y = (Cntz ` H )   =>    |- ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> ( F ` A ) e. ( Y ` ( F " S ) ) )
Theorem	cntzmhm2 15093	Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- Z = (Cntz ` G )   &    |- Y = (Cntz ` H )   =>    |- ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> ( F " S ) C_ ( Y ` ( F " T ) ) )
Theorem	cntrsubgnsg 15094	A central subgroup is normal. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- Z = (Cntr ` M )   =>    |- ( ( X e. (SubGrp ` M ) /\ X C_ Z ) -> X e. (NrmSGrp ` M ) )
Theorem	cntrnsg 15095	The center of a group is a normal subgroup. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- Z = (Cntr ` M )   =>    |- ( M e. Grp -> Z e. (NrmSGrp ` M ) )
10.2.8  The opposite group
Syntax	coppg 15096	The opposite group operation.
class oppg
Definition	df-oppg 15097	Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr 15683 does the same thing for multiplication. (Contributed by Stefan O'Rear, 25-Aug-2015.)
|- oppg = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , tpos ( +g ` w ) >. ) )
Theorem	oppgval 15098	Value of the opposite group. (Contributed by Stefan O'Rear, 25-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.) (Revised by Fan Zheng, 26-Jun-2016.)
|- .+ = ( +g ` R )   &    |- O = (oppg ` R )   =>    |- O = ( R sSet <. ( +g ` ndx ) , tpos .+ >. )
Theorem	oppgplusfval 15099	Value of the addition operation of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Fan Zheng, 26-Jun-2016.)
|- .+ = ( +g ` R )   &    |- O = (oppg ` R )   &    |- .+b = ( +g ` O )   =>    |- .+b = tpos .+
Theorem	oppgplus 15100	Value of the addition operation of an opposite ring. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Fan Zheng, 26-Jun-2016.)
|- .+ = ( +g ` R )   &    |- O = (oppg ` R )   &    |- .+b = ( +g ` O )   =>    |- ( X .+b Y ) = ( Y .+ X )