P. 171 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	ga0 17001	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 17002	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 17003*	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 17004*	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 17005	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 17006*	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 17007	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 17008	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 = ( invg ` G )   =>    |- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A .(+) B ) = C <-> ( ( N ` A ) .(+) C ) = B ) )
Theorem	gapm 17009*	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 17010*	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 17011*	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 17012*	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 17013*	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 17014*	Existence and uniqueness for the function of orbsta 17016. (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 17015*	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 17016*	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 17017*	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  Centralizers and centers
Syntax	ccntz 17018	Syntax for the centralizer of a set in a monoid.
class Cntz
Syntax	ccntr 17019	Syntax for the centralizer of a monoid.
class Cntr
Definition	df-cntz 17020*	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 17021	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 17022	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 17023*	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 17024*	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 17025*	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 17026*	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 17027*	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 17028	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 17029*	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 17030	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 17031	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 17032	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 17033	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 17034	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 17035	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 17036	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 17037*	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 17038	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 17039	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 17040	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 17041	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 17042	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 17043	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 17044	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.7  The opposite group
Syntax	coppg 17045	The opposite group operation.
class oppg
Definition	df-oppg 17046	Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr 17900 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 17047	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 17048	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 17049	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 )
Theorem	oppglem 17050	Lemma for oppgbas 17051. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- O = (oppg ` R )   &    |- E = Slot N   &    |- N e. NN   &    |- N =/= 2   =>    |- ( E ` R ) = ( E ` O )
Theorem	oppgbas 17051	Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- O = (oppg ` R )   &    |- B = ( Base ` R )   =>    |- B = ( Base ` O )
Theorem	oppgtset 17052	Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.)
|- O = (oppg ` R )   &    |- J = (TopSet ` R )   =>    |- J = (TopSet ` O )
Theorem	oppgtopn 17053	Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.)
|- O = (oppg ` R )   &    |- J = ( TopOpen ` R )   =>    |- J = ( TopOpen ` O )
Theorem	oppgmnd 17054	The opposite of a monoid is a monoid. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.)
|- O = (oppg ` R )   =>    |- ( R e. Mnd -> O e. Mnd )
Theorem	oppgmndb 17055	Bidirectional form of oppgmnd 17054. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- O = (oppg ` R )   =>    |- ( R e. Mnd <-> O e. Mnd )
Theorem	oppgid 17056	Zero in a monoid is a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.)
|- O = (oppg ` R )   &    |- .0. = ( 0g ` R )   =>    |- .0. = ( 0g ` O )
Theorem	oppggrp 17057	The opposite of a group is a group. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- O = (oppg ` R )   =>    |- ( R e. Grp -> O e. Grp )
Theorem	oppggrpb 17058	Bidirectional form of oppggrp 17057. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- O = (oppg ` R )   =>    |- ( R e. Grp <-> O e. Grp )
Theorem	oppginv 17059	Inverses in a group are a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- O = (oppg ` R )   &    |- I = ( invg ` R )   =>    |- ( R e. Grp -> I = ( invg ` O ) )
Theorem	invoppggim 17060	The inverse is an antiautomorphism on any group. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- O = (oppg ` G )   &    |- I = ( invg ` G )   =>    |- ( G e. Grp -> I e. ( G GrpIso O ) )
Theorem	oppggic 17061	Every group is (naturally) isomorphic to its opposite. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- O = (oppg ` G )   =>    |- ( G e. Grp -> G ~=g𝑔 O )
Theorem	oppgsubm 17062	Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.)
|- O = (oppg ` G )   =>    |- (SubMnd ` G ) = (SubMnd ` O )
Theorem	oppgsubg 17063	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.)
|- O = (oppg ` G )   =>    |- (SubGrp ` G ) = (SubGrp ` O )
Theorem	oppgcntz 17064	A centralizer in a group is the same as the centralizer in the opposite group. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- O = (oppg ` G )   &    |- Z = (Cntz ` G )   =>    |- ( Z ` A ) = ( (Cntz ` O ) ` A )
Theorem	oppgcntr 17065	The center of a group is the same as the center of the opposite group. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- O = (oppg ` G )   &    |- Z = (Cntr ` G )   =>    |- Z = (Cntr ` O )
Theorem	gsumwrev 17066	A sum in an opposite monoid is the regular sum of a reversed word. (Contributed by Stefan O'Rear, 27-Aug-2015.) (Proof shortened by Mario Carneiro, 28-Feb-2016.)
|- B = ( Base ` M )   &    |- O = (oppg ` M )   =>    |- ( ( M e. Mnd /\ W e. Word B ) -> ( O gsumg W ) = ( M gsumg (reverse ` W ) ) )
10.2.8  Symmetric groups
10.2.8.1  Definition and basic properties According to Wikipedia ("Symmetric group", 09-Mar-2019, https://en.wikipedia.org/wiki/symmetric_group) "In abstract algebra, the symmetric group defined over any set is the group whose elements are all the bijections from the set to itself, and whose group operation is the composition of functions." and according to Encyclopedia of Mathematics ("Symmetric group", 09-Mar-2019, https://www.encyclopediaofmath.org/index.php/Symmetric_group) "The group of all permutations (self-bijections) of a set with the operation of composition (see Permutation group).". In [Rotman] p. 27 "If X is a nonempty set, a permutation of X is a function a : X -> X that is a one-to-one correspondence." and "If X is a nonempty set, the symmetric group on X, denoted SX, is the group whose elements are the permutations of X and whose binary operation is composition of functions.". Therefore, we define the symmetric group on a set A as the set of one-to-one onto functions from A to itself under function composition, see df-symg 17068. However, the set is allowed to be empty, see symgbas0 17084. Hint: The symmetric groups should not be confused with "symmetry groups" which is a different topic in group theory. In this context, the one-to-one onto functions are called permutations for short. Since the base set of symmetric groups on a set A is the set of all permutations of A (see symgbas 17070), we can formally say P e. ( SymGrp ` A ) expressing " P is a permutation of A" if we are not interested in the group (or topology) structure. In general, a permutation group "... is a group G whose elements are permutations of a given set M and whose group operation is the composition of permutations in G (which are thought of as bijective functions from the set M to itself)." (see Wikipedia "Permutation group", 17-Mar-2019, https://en.wikipedia.org/wiki/Permutation_group). This means that a symmetric group is a permutation group, and each permutation group is a subgroup of a symmetric group (see pgrpsubgsymgbi 17097 and pgrpsubgsymg 17098). For example, the structure with the singleton containing only the identity function restricted to a set as base set and the function composition as group operation is a permutation group (group consisting of permutations), see idrespermg 17101, which is a (proper) subgroup of a symmetric group, see idressubgsymg 17100. As in [Rotman] p. 28 "Let x e. X and p e. SymGrp ( X ); we say p fixes x if ( p ` x ) = x; otherwise p moves x.". The theorems starting with symgfix2 17106 are about fixed/moved elements.
Syntax	csymg 17067	Extend class notation to include the class of symmetric groups.
class SymGrp
Definition	df-symg 17068*	Define the symmetric group on set x. We represent the group as the set of one-to-one 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 17069*	The value of the symmetric 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 17070*	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 17071	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 17072	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	symgbasf1o 17073	Elements in the symmetric group are 1-1 onto functions. (Contributed by SO, 9-Jul-2018.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   =>    |- ( F e. B -> F : A -1-1-onto-> A )
Theorem	symgbasf 17074	A permutation (element of the symmetric group) is a function of a set into itself. (Contributed by AV, 1-Jan-2019.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   =>    |- ( F e. B -> F : A --> A )
Theorem	symghash 17075	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	symgbasfi 17076	The symmetric group on a finite index set is finite. (Contributed by SO, 9-Jul-2018.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   =>    |- ( A e. Fin -> B e. Fin )
Theorem	symgfv 17077	The function value of a permutation. (Contributed by AV, 1-Jan-2019.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   =>    |- ( ( F e. B /\ X e. A ) -> ( F ` X ) e. A )
Theorem	symgfvne 17078	The function values of a permutation for different arguments are different. (Contributed by AV, 8-Jan-2019.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   =>    |- ( ( F e. B /\ X e. A /\ Y e. A ) -> ( ( F ` X ) = Z -> ( Y =/= X -> ( F ` Y ) =/= Z ) ) )
Theorem	symgplusg 17079*	The group operation of a symmetric group is the function composition. (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 17080	The value of the group operation of the symmetric 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 17081	The group operation of the symmetric 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	symgmov1 17082*	For a permutation of a set, each element of the set replaces an(other) element of the set. (Contributed by AV, 2-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   =>    |- ( Q e. P -> A. n e. N E. k e. N ( Q ` n ) = k )
Theorem	symgmov2 17083*	For a permutation of a set, each element of the set is replaced by an(other) element of the set. (Contributed by AV, 2-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   =>    |- ( Q e. P -> A. n e. N E. k e. N ( Q ` k ) = n )
Theorem	symgbas0 17084	The base set of the symmetric group on the empty set is the singleton containing the empty set. (Contributed by AV, 27-Feb-2019.)
|- ( Base ` ( SymGrp ` (/) ) ) = { (/) }
Theorem	symg1hash 17085	The symmetric group on a singleton has cardinality 1. (Contributed by AV, 9-Dec-2018.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   &    |- A = { I }   =>    |- ( I e. V -> ( # ` B ) = 1 )
Theorem	symg1bas 17086	The symmetric group on a singleton is the symmetric group S1 consisting of the identity only. (Contributed by AV, 9-Dec-2018.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   &    |- A = { I }   =>    |- ( I e. V -> B = { { <. I , I >. } } )
Theorem	symg2hash 17087	The symmetric group on a (proper) pair has cardinality 2. (Contributed by AV, 9-Dec-2018.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   &    |- A = { I , J }   =>    |- ( ( I e. V /\ J e. W /\ I =/= J ) -> ( # ` B ) = 2 )
Theorem	symg2bas 17088	The symmetric group on a pair is the symmetric group S2 consisting of the identity and the transposition. This theorem is also valid if the elements are identical: then it collapses to theorem symg1bas 17086. (Contributed by AV, 9-Dec-2018.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   &    |- A = { I , J }   =>    |- ( ( I e. V /\ J e. W ) -> B = { { <. I , I >. , <. J , J >. } , { <. I , J >. , <. J , I >. } } )
Theorem	symgtset 17089	The topology of the symmetric 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 17090	The symmetric group on a set 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 17091	The group identity element of the symmetric group on a set 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 17092	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 = ( invg ` G )   =>    |- ( F e. B -> ( N ` F ) = `' F )
Theorem	galactghm 17093*	The currying of a group action is a group homomorphism between the group G and the symmetric 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 17094*	The converse of galactghm 17093. 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 17095	The topology of the symmetric 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 17096*	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	pgrpsubgsymgbi 17097	Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   =>    |- ( A e. V -> ( P e. (SubGrp ` G ) <-> ( P C_ B /\ ( G ↾s P ) e. Grp ) ) )
Theorem	pgrpsubgsymg 17098*	Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   &    |- F = ( Base ` P )   =>    |- ( A e. V -> ( ( P e. Grp /\ F C_ B /\ ( +g ` P ) = ( f e. F , g e. F |-> ( f o. g ) ) ) -> F e. (SubGrp ` G ) ) )
Theorem	idresperm 17099	The identity function restricted to a set is a permutation of this set. (Contributed by AV, 17-Mar-2019.)
|- G = ( SymGrp ` A )   =>    |- ( A e. V -> ( _I |` A ) e. ( Base ` G ) )
Theorem	idressubgsymg 17100	The singleton containing only the identity function restricted to a set is a subgroup of the symmetric group of this set. (Contributed by AV, 17-Mar-2019.)
|- G = ( SymGrp ` A )   =>    |- ( A e. V -> { ( _I |` A ) } e. (SubGrp ` G ) )