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	idresperm 17001	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 17002	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 ) )
Theorem	idrespermg 17003	The structure with the singleton containing only the identity function restricted to a set as base set and the function composition as group operation (constructed by (structure) restricting the symmetric group to that singleton) is a permutation group (group consisting of permutations). (Contributed by AV, 17-Mar-2019.)
|- G = ( SymGrp ` A )   &    |- E = ( G ↾s { ( _I |` A ) } )   =>    |- ( A e. V -> ( E e. Grp /\ ( Base ` E ) C_ ( Base ` G ) ) )
10.2.8.2  Cayley's theorem
Theorem	cayleylem1 17004*	Lemma for cayley 17006. (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 17005*	Lemma for cayley 17006. (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 17006*	Cayley's Theorem (constructive version): given group G, F is an isomorphism between G and the subgroup S of the symmetric group H on the underlying set X of G. See also Theorem 3.15 in [Rotman] p. 42. (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 17007*	Cayley's Theorem (existence version): every group G is isomorphic to a subgroup of the symmetric group on the underlying set of G. (For any group G there exists an isomorphism f between G and a subgroup h of the symmetric group on the underlying set of G.) See also Theorem 3.15 in [Rotman] p. 42. (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.8.3  Permutations fixing one element
Theorem	symgfix2 17008*	If a permutation does not move a certain element of a set to a second element, there is a third element which is moved to the second element. (Contributed by AV, 2-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   =>    |- ( L e. N -> ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> E. k e. ( N \ { K } ) ( Q ` k ) = L ) )
Theorem	symgextf 17009*	The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019.)
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )   =>    |- ( ( K e. N /\ Z e. S ) -> E : N --> N )
Theorem	symgextfv 17010*	The function value of the extension of a permutation, fixing the additional element, for elements in the original domain. (Contributed by AV, 6-Jan-2019.)
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )   =>    |- ( ( K e. N /\ Z e. S ) -> ( X e. ( N \ { K } ) -> ( E ` X ) = ( Z ` X ) ) )
Theorem	symgextfve 17011*	The function value of the extension of a permutation, fixing the additional element, for the additional element. (Contributed by AV, 6-Jan-2019.)
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )   =>    |- ( K e. N -> ( X = K -> ( E ` X ) = K ) )
Theorem	symgextf1lem 17012*	Lemma for symgextf1 17013. (Contributed by AV, 6-Jan-2019.)
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )   =>    |- ( ( K e. N /\ Z e. S ) -> ( ( X e. ( N \ { K } ) /\ Y e. { K } ) -> ( E ` X ) =/= ( E ` Y ) ) )
Theorem	symgextf1 17013*	The extension of a permutation, fixing the additional element, is a 1-1 function. (Contributed by AV, 6-Jan-2019.)
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )   =>    |- ( ( K e. N /\ Z e. S ) -> E : N -1-1-> N )
Theorem	symgextfo 17014*	The extension of a permutation, fixing the additional element, is an onto function. (Contributed by AV, 7-Jan-2019.)
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )   =>    |- ( ( K e. N /\ Z e. S ) -> E : N -onto-> N )
Theorem	symgextf1o 17015*	The extension of a permutation, fixing the additional element, is a bijection. (Contributed by AV, 7-Jan-2019.)
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )   =>    |- ( ( K e. N /\ Z e. S ) -> E : N -1-1-onto-> N )
Theorem	symgextsymg 17016*	The extension of a permutation is an element of the extended symmetric group. (Contributed by AV, 9-Mar-2019.)
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )   =>    |- ( ( N e. V /\ K e. N /\ Z e. S ) -> E e. ( Base ` ( SymGrp ` N ) ) )
Theorem	symgextres 17017*	The restriction of the extension of a permutation, fixing the additional element, to the original domain. (Contributed by AV, 6-Jan-2019.)
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )   =>    |- ( ( K e. N /\ Z e. S ) -> ( E |` ( N \ { K } ) ) = Z )
Theorem	gsumccatsymgsn 17018	Homomorphic property of composites of permutations with a singleton. (Contributed by AV, 20-Jan-2019.)
|- G = ( SymGrp ` A )   &    |- B = ( Base ` G )   =>    |- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( G gsumg ( W ++ <" Z "> ) ) = ( ( G gsumg W ) o. Z ) )
Theorem	gsmsymgrfixlem1 17019*	Lemma 1 for gsmsymgrfix 17020. (Contributed by AV, 20-Jan-2019.)
|- S = ( SymGrp ` N )   &    |- B = ( Base ` S )   =>    |- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsumg W ) ` K ) = K ) ) -> ( A. i e. ( 0..^ ( ( # ` W ) + 1 ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K -> ( ( S gsumg ( W ++ <" P "> ) ) ` K ) = K ) )
Theorem	gsmsymgrfix 17020*	The composition of permutations fixing one element also fixes this element. (Contributed by AV, 20-Jan-2019.)
|- S = ( SymGrp ` N )   &    |- B = ( Base ` S )   =>    |- ( ( N e. Fin /\ K e. N /\ W e. Word B ) -> ( A. i e. ( 0..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsumg W ) ` K ) = K ) )
Theorem	fvcosymgeq 17021*	The values of two compositions of permutations are equal if the values of the composed permutations are pairwise equal. (Contributed by AV, 26-Jan-2019.)
|- S = ( SymGrp ` N )   &    |- B = ( Base ` S )   &    |- Z = ( SymGrp ` M )   &    |- P = ( Base ` Z )   &    |- I = ( N i^i M )   =>    |- ( ( G e. B /\ K e. P ) -> ( ( X e. I /\ ( G ` X ) = ( K ` X ) /\ A. n e. I ( F ` n ) = ( H ` n ) ) -> ( ( F o. G ) ` X ) = ( ( H o. K ) ` X ) ) )
Theorem	gsmsymgreqlem1 17022*	Lemma 1 for gsmsymgreq 17024. (Contributed by AV, 26-Jan-2019.)
|- S = ( SymGrp ` N )   &    |- B = ( Base ` S )   &    |- Z = ( SymGrp ` M )   &    |- P = ( Base ` Z )   &    |- I = ( N i^i M )   =>    |- ( ( ( N e. Fin /\ M e. Fin /\ J e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> ( ( A. n e. I ( ( S gsumg X ) ` n ) = ( ( Z gsumg Y ) ` n ) /\ ( C ` J ) = ( R ` J ) ) -> ( ( S gsumg ( X ++ <" C "> ) ) ` J ) = ( ( Z gsumg ( Y ++ <" R "> ) ) ` J ) ) )
Theorem	gsmsymgreqlem2 17023*	Lemma 2 for gsmsymgreq 17024. (Contributed by AV, 26-Jan-2019.)
|- S = ( SymGrp ` N )   &    |- B = ( Base ` S )   &    |- Z = ( SymGrp ` M )   &    |- P = ( Base ` Z )   &    |- I = ( N i^i M )   =>    |- ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> ( ( A. i e. ( 0..^ ( # ` X ) ) A. n e. I ( ( X ` i ) ` n ) = ( ( Y ` i ) ` n ) -> A. n e. I ( ( S gsumg X ) ` n ) = ( ( Z gsumg Y ) ` n ) ) -> ( A. i e. ( 0..^ ( # ` ( X ++ <" C "> ) ) ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) -> A. n e. I ( ( S gsumg ( X ++ <" C "> ) ) ` n ) = ( ( Z gsumg ( Y ++ <" R "> ) ) ` n ) ) ) )
Theorem	gsmsymgreq 17024*	Two combination of permutations moves an element of the intersection of the base sets of the permutations to the same element if each pair of corresponding permutations moves such an element to the same element. (Contributed by AV, 20-Jan-2019.)
|- S = ( SymGrp ` N )   &    |- B = ( Base ` S )   &    |- Z = ( SymGrp ` M )   &    |- P = ( Base ` Z )   &    |- I = ( N i^i M )   =>    |- ( ( ( N e. Fin /\ M e. Fin ) /\ ( W e. Word B /\ U e. Word P /\ ( # ` W ) = ( # ` U ) ) ) -> ( A. i e. ( 0..^ ( # ` W ) ) A. n e. I ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) -> A. n e. I ( ( S gsumg W ) ` n ) = ( ( Z gsumg U ) ` n ) ) )
Theorem	symgfixelq 17025*	A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- Q = { q e. P | ( q ` K ) = K }   =>    |- ( F e. V -> ( F e. Q <-> ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) )
Theorem	symgfixels 17026*	The restriction of a permutation to a set with one element removed is an element of the restricted symmetric group if the restriction is a 1-1 onto function. (Contributed by AV, 4-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- Q = { q e. P | ( q ` K ) = K }   &    |- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- D = ( N \ { K } )   =>    |- ( F e. V -> ( ( F |` D ) e. S <-> ( F |` D ) : D -1-1-onto-> D ) )
Theorem	symgfixelsi 17027*	The restriction of a permutation fixing an element to the set with this element removed is an element of the restricted symmetric group. (Contributed by AV, 4-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- Q = { q e. P | ( q ` K ) = K }   &    |- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- D = ( N \ { K } )   =>    |- ( ( K e. N /\ F e. Q ) -> ( F |` D ) e. S )
Theorem	symgfixf 17028*	The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a function. (Contributed by AV, 4-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- Q = { q e. P | ( q ` K ) = K }   &    |- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )   =>    |- ( K e. N -> H : Q --> S )
Theorem	symgfixf1 17029*	The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a 1-1 function. (Contributed by AV, 4-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- Q = { q e. P | ( q ` K ) = K }   &    |- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )   =>    |- ( K e. N -> H : Q -1-1-> S )
Theorem	symgfixfolem1 17030*	Lemma 1 for symgfixfo 17031. (Contributed by AV, 7-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- Q = { q e. P | ( q ` K ) = K }   &    |- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )   &    |- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )   =>    |- ( ( N e. V /\ K e. N /\ Z e. S ) -> E e. Q )
Theorem	symgfixfo 17031*	The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is an onto function. (Contributed by AV, 7-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- Q = { q e. P | ( q ` K ) = K }   &    |- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )   =>    |- ( ( N e. V /\ K e. N ) -> H : Q -onto-> S )
Theorem	symgfixf1o 17032*	The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a bijection. (Contributed by AV, 7-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- Q = { q e. P | ( q ` K ) = K }   &    |- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )   =>    |- ( ( N e. V /\ K e. N ) -> H : Q -1-1-onto-> S )
10.2.8.4  Transpositions in the symmetric group Transpositions are special cases of "cycles" as defined in [Rotman] p. 28: "Let i1 , i2 , ... , ir be distinct integers between 1 and n. If α in Sn fixes the other integers and α(i1) = i2, α(i2) = i3, ..., α(ir-1 ) = ir, α(ir) = i1, then α is an r-cycle. We also say that α is a cycle of length r." and in [Rotman] p. 31: "A 2-cycle is also called transposition.". We (currently) do not have/need a definition for cycles, so transpositions are explicitly defined in df-pmtr 17034.
Syntax	cpmtr 17033	Syntax for the transposition generator function.
class pmTrsp
Definition	df-pmtr 17034*	Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.)
|- pmTrsp = ( d e. _V |-> ( p e. { y e. ~P d | y ~~ 2o } |-> ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
Theorem	f1omvdmvd 17035	A permutation of any class moves a point which is moved to a different point which is moved. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> ( F ` X ) e. ( dom ( F \ _I ) \ { X } ) )
Theorem	f1omvdcnv 17036	A permutation and its inverse move the same points. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- ( F : A -1-1-onto-> A -> dom ( `' F \ _I ) = dom ( F \ _I ) )
Theorem	mvdco 17037	Composing two permutations moves at most the union of the points. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- dom ( ( F o. G ) \ _I ) C_ ( dom ( F \ _I ) u. dom ( G \ _I ) )
Theorem	f1omvdconj 17038	Conjugation of a permutation takes the image of the moved subclass. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- ( ( F : A --> A /\ G : A -1-1-onto-> A ) -> dom ( ( ( G o. F ) o. `' G ) \ _I ) = ( G " dom ( F \ _I ) ) )
Theorem	f1otrspeq 17039	A transposition is characterized by the points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> F = G )
Theorem	f1omvdco2 17040	If exactly one of two permutations is limited to a set of points, then the composition will not be. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A /\ ( dom ( F \ _I ) C_ X \/_ dom ( G \ _I ) C_ X ) ) -> -. dom ( ( F o. G ) \ _I ) C_ X )
Theorem	f1omvdco3 17041	If a point is moved by exactly one of two permutations, then it will be moved by their composite. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A /\ ( X e. dom ( F \ _I ) \/_ X e. dom ( G \ _I ) ) ) -> X e. dom ( ( F o. G ) \ _I ) )
Theorem	pmtrfval 17042*	The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.)
|- T = (pmTrsp ` D )   =>    |- ( D e. V -> T = ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
Theorem	pmtrval 17043*	A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015.)
|- T = (pmTrsp ` D )   =>    |- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) = ( z e. D |-> if ( z e. P , U. ( P \ { z } ) , z ) ) )
Theorem	pmtrfv 17044	General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.)
|- T = (pmTrsp ` D )   =>    |- ( ( ( D e. V /\ P C_ D /\ P ~~ 2o ) /\ Z e. D ) -> ( ( T ` P ) ` Z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) )
Theorem	pmtrprfv 17045	In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015.)
|- T = (pmTrsp ` D )   =>    |- ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> ( ( T ` { X , Y } ) ` X ) = Y )
Theorem	pmtrprfv3 17046	In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019.)
|- T = (pmTrsp ` D )   =>    |- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( T ` { X , Y } ) ` Z ) = Z )
Theorem	pmtrf 17047	Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.)
|- T = (pmTrsp ` D )   =>    |- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) : D --> D )
Theorem	pmtrmvd 17048	A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.)
|- T = (pmTrsp ` D )   =>    |- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> dom ( ( T ` P ) \ _I ) = P )
Theorem	pmtrrn 17049	Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- T = (pmTrsp ` D )   &    |- R = ran T   =>    |- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) e. R )
Theorem	pmtrfrn 17050	A transposition (as a kind of function) is the function transposing the two points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- T = (pmTrsp ` D )   &    |- R = ran T   &    |- P = dom ( F \ _I )   =>    |- ( F e. R -> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) )
Theorem	pmtrffv 17051	Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- T = (pmTrsp ` D )   &    |- R = ran T   &    |- P = dom ( F \ _I )   =>    |- ( ( F e. R /\ Z e. D ) -> ( F ` Z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) )
Theorem	pmtrrn2 17052*	For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018.)
|- T = (pmTrsp ` D )   &    |- R = ran T   =>    |- ( F e. R -> E. x e. D E. y e. D ( x =/= y /\ F = ( T ` { x , y } ) ) )
Theorem	pmtrfinv 17053	A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- T = (pmTrsp ` D )   &    |- R = ran T   =>    |- ( F e. R -> ( F o. F ) = ( _I |` D ) )
Theorem	pmtrfmvdn0 17054	A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- T = (pmTrsp ` D )   &    |- R = ran T   =>    |- ( F e. R -> dom ( F \ _I ) =/= (/) )
Theorem	pmtrff1o 17055	A transposition function is a permutation. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- T = (pmTrsp ` D )   &    |- R = ran T   =>    |- ( F e. R -> F : D -1-1-onto-> D )
Theorem	pmtrfcnv 17056	A transposition function is its own inverse. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- T = (pmTrsp ` D )   &    |- R = ran T   =>    |- ( F e. R -> `' F = F )
Theorem	pmtrfb 17057	An intrinsic characterization of the transposition permutations. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- T = (pmTrsp ` D )   &    |- R = ran T   =>    |- ( F e. R <-> ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) )
Theorem	pmtrfconj 17058	Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- T = (pmTrsp ` D )   &    |- R = ran T   =>    |- ( ( F e. R /\ G : D -1-1-onto-> D ) -> ( ( G o. F ) o. `' G ) e. R )
Theorem	symgsssg 17059*	The symmetric group has subgroups restricting the set of non-fixed points. (Contributed by Stefan O'Rear, 24-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   =>    |- ( D e. V -> { x e. B | dom ( x \ _I ) C_ X } e. (SubGrp ` G ) )
Theorem	symgfisg 17060*	The symmetric group has a subgroup of permutations that move finitely many points. (Contributed by Stefan O'Rear, 24-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   =>    |- ( D e. V -> { x e. B | dom ( x \ _I ) e. Fin } e. (SubGrp ` G ) )
Theorem	symgtrf 17061	Transpositions are elements of the symmetric group. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- T = ran (pmTrsp ` D )   &    |- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   =>    |- T C_ B
Theorem	symggen 17062*	The span of the transpositions is the subgroup that moves finitely many points. (Contributed by Stefan O'Rear, 28-Aug-2015.)
|- T = ran (pmTrsp ` D )   &    |- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   &    |- K = (mrCls ` (SubMnd ` G ) )   =>    |- ( D e. V -> ( K ` T ) = { x e. B | dom ( x \ _I ) e. Fin } )
Theorem	symggen2 17063	A finite permutation group is generated by the transpositions, see also Theorem 3.4 in [Rotman] p. 31. (Contributed by Stefan O'Rear, 28-Aug-2015.)
|- T = ran (pmTrsp ` D )   &    |- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   &    |- K = (mrCls ` (SubMnd ` G ) )   =>    |- ( D e. Fin -> ( K ` T ) = B )
Theorem	symgtrinv 17064	To invert a permutation represented as a sequence of transpositions, reverse the sequence. (Contributed by Stefan O'Rear, 27-Aug-2015.)
|- T = ran (pmTrsp ` D )   &    |- G = ( SymGrp ` D )   &    |- I = ( invg ` G )   =>    |- ( ( D e. V /\ W e. Word T ) -> ( I ` ( G gsumg W ) ) = ( G gsumg (reverse ` W ) ) )
Theorem	pmtr3ncomlem1 17065	Lemma 1 for pmtr3ncom 17067. (Contributed by AV, 17-Mar-2018.)
|- T = (pmTrsp ` D )   &    |- F = ( T ` { X , Y } )   &    |- G = ( T ` { Y , Z } )   =>    |- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( G o. F ) ` X ) =/= ( ( F o. G ) ` X ) )
Theorem	pmtr3ncomlem2 17066	Lemma 2 for pmtr3ncom 17067. (Contributed by AV, 17-Mar-2018.)
|- T = (pmTrsp ` D )   &    |- F = ( T ` { X , Y } )   &    |- G = ( T ` { Y , Z } )   =>    |- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( G o. F ) =/= ( F o. G ) )
Theorem	pmtr3ncom 17067*	Transpositions over sets with at least 3 elements are not commutative, see also the remark in [Rotman] p. 28. (Contributed by AV, 21-Mar-2019.)
|- T = (pmTrsp ` D )   =>    |- ( ( D e. V /\ 3 <_ ( # ` D ) ) -> E. f e. ran T E. g e. ran T ( g o. f ) =/= ( f o. g ) )
Theorem	pmtrdifellem1 17068	Lemma 1 for pmtrdifel 17072. (Contributed by AV, 15-Jan-2019.)
|- T = ran (pmTrsp ` ( N \ { K } ) )   &    |- R = ran (pmTrsp ` N )   &    |- S = ( (pmTrsp ` N ) ` dom ( Q \ _I ) )   =>    |- ( Q e. T -> S e. R )
Theorem	pmtrdifellem2 17069	Lemma 2 for pmtrdifel 17072. (Contributed by AV, 15-Jan-2019.)
|- T = ran (pmTrsp ` ( N \ { K } ) )   &    |- R = ran (pmTrsp ` N )   &    |- S = ( (pmTrsp ` N ) ` dom ( Q \ _I ) )   =>    |- ( Q e. T -> dom ( S \ _I ) = dom ( Q \ _I ) )
Theorem	pmtrdifellem3 17070*	Lemma 3 for pmtrdifel 17072. (Contributed by AV, 15-Jan-2019.)
|- T = ran (pmTrsp ` ( N \ { K } ) )   &    |- R = ran (pmTrsp ` N )   &    |- S = ( (pmTrsp ` N ) ` dom ( Q \ _I ) )   =>    |- ( Q e. T -> A. x e. ( N \ { K } ) ( Q ` x ) = ( S ` x ) )
Theorem	pmtrdifellem4 17071	Lemma 4 for pmtrdifel 17072. (Contributed by AV, 28-Jan-2019.)
|- T = ran (pmTrsp ` ( N \ { K } ) )   &    |- R = ran (pmTrsp ` N )   &    |- S = ( (pmTrsp ` N ) ` dom ( Q \ _I ) )   =>    |- ( ( Q e. T /\ K e. N ) -> ( S ` K ) = K )
Theorem	pmtrdifel 17072*	A transposition of elements of a set without a special element corresponds to a transposition of elements of the set. (Contributed by AV, 15-Jan-2019.)
|- T = ran (pmTrsp ` ( N \ { K } ) )   &    |- R = ran (pmTrsp ` N )   =>    |- A. t e. T E. r e. R A. x e. ( N \ { K } ) ( t ` x ) = ( r ` x )
Theorem	pmtrdifwrdellem1 17073*	Lemma 1 for pmtrdifwrdel 17077. (Contributed by AV, 15-Jan-2019.)
|- T = ran (pmTrsp ` ( N \ { K } ) )   &    |- R = ran (pmTrsp ` N )   &    |- U = ( x e. ( 0..^ ( # ` W ) ) |-> ( (pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) )   =>    |- ( W e. Word T -> U e. Word R )
Theorem	pmtrdifwrdellem2 17074*	Lemma 2 for pmtrdifwrdel 17077. (Contributed by AV, 15-Jan-2019.)
|- T = ran (pmTrsp ` ( N \ { K } ) )   &    |- R = ran (pmTrsp ` N )   &    |- U = ( x e. ( 0..^ ( # ` W ) ) |-> ( (pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) )   =>    |- ( W e. Word T -> ( # ` W ) = ( # ` U ) )
Theorem	pmtrdifwrdellem3 17075*	Lemma 3 for pmtrdifwrdel 17077. (Contributed by AV, 15-Jan-2019.)
|- T = ran (pmTrsp ` ( N \ { K } ) )   &    |- R = ran (pmTrsp ` N )   &    |- U = ( x e. ( 0..^ ( # ` W ) ) |-> ( (pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) )   =>    |- ( W e. Word T -> A. i e. ( 0..^ ( # ` W ) ) A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) )
Theorem	pmtrdifwrdel2lem1 17076*	Lemma 1 for pmtrdifwrdel2 17078. (Contributed by AV, 31-Jan-2019.)
|- T = ran (pmTrsp ` ( N \ { K } ) )   &    |- R = ran (pmTrsp ` N )   &    |- U = ( x e. ( 0..^ ( # ` W ) ) |-> ( (pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) )   =>    |- ( ( W e. Word T /\ K e. N ) -> A. i e. ( 0..^ ( # ` W ) ) ( ( U ` i ) ` K ) = K )
Theorem	pmtrdifwrdel 17077*	A sequence of transpositions of elements of a set without a special element corresponds to a sequence of transpositions of elements of the set. (Contributed by AV, 15-Jan-2019.)
|- T = ran (pmTrsp ` ( N \ { K } ) )   &    |- R = ran (pmTrsp ` N )   =>    |- A. w e. Word T E. u e. Word R ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) )
Theorem	pmtrdifwrdel2 17078*	A sequence of transpositions of elements of a set without a special element corresponds to a sequence of transpositions of elements of the set not moving the special element. (Contributed by AV, 31-Jan-2019.)
|- T = ran (pmTrsp ` ( N \ { K } ) )   &    |- R = ran (pmTrsp ` N )   =>    |- ( K e. N -> A. w e. Word T E. u e. Word R ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0..^ ( # ` w ) ) ( ( ( u ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) ) )
Theorem	pmtrprfval 17079*	The transpositions on a pair. (Contributed by AV, 9-Dec-2018.)
|- (pmTrsp ` { 1 , 2 } ) = ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) )
Theorem	pmtrprfvalrn 17080	The range of the transpositions on a pair is actually a singleton: the transposition of the two elements of the pair. (Contributed by AV, 9-Dec-2018.)
|- ran (pmTrsp ` { 1 , 2 } ) = { { <. 1 , 2 >. , <. 2 , 1 >. } }
10.2.8.5  The sign of a permutation
Syntax	cpsgn 17081	Syntax for the sign of a permutation.
class pmSgn
Syntax	cevpm 17082	Syntax for even permutations.
class pmEven
Definition	df-psgn 17083*	Define a function which takes the value 1 for even permutations and -u 1 for odd. (Contributed by Stefan O'Rear, 28-Aug-2015.)
|- pmSgn = ( d e. _V |-> ( x e. { p e. ( Base ` ( SymGrp ` d ) ) | dom ( p \ _I ) e. Fin } |-> ( iota s E. w e. Word ran (pmTrsp ` d ) ( x = ( ( SymGrp ` d ) gsumg w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) )
Definition	df-evpm 17084	Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018.)
|- pmEven = ( d e. _V |-> ( `' (pmSgn ` d ) " { 1 } ) )
Theorem	psgnunilem1 17085*	Lemma for psgnuni 17091. Given two consequtive transpositions in a representation of a permutation, either they are equal and therefore equivalent to the identity, or they are not and it is possible to commute them such that a chosen point in the left transposition is preserved in the right. By repeating this process, a point can be removed from a representation of the identity. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- T = ran (pmTrsp ` D )   &    |- ( ph -> D e. V )   &    |- ( ph -> P e. T )   &    |- ( ph -> Q e. T )   &    |- ( ph -> A e. dom ( P \ _I ) )   =>    |- ( ph -> ( ( P o. Q ) = ( _I |` D ) \/ E. r e. T E. s e. T ( ( P o. Q ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) )
Theorem	psgnunilem5 17086*	Lemma for psgnuni 17091. It is impossible to shift a transposition off the end because if the active transposition is at the right end, it is the only transposition moving A in contradiction to this being a representation of the identity. (Contributed by Stefan O'Rear, 25-Aug-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
|- G = ( SymGrp ` D )   &    |- T = ran (pmTrsp ` D )   &    |- ( ph -> D e. V )   &    |- ( ph -> W e. Word T )   &    |- ( ph -> ( G gsumg W ) = ( _I |` D ) )   &    |- ( ph -> ( # ` W ) = L )   &    |- ( ph -> I e. ( 0..^ L ) )   &    |- ( ph -> A e. dom ( ( W ` I ) \ _I ) )   &    |- ( ph -> A. k e. ( 0..^ I ) -. A e. dom ( ( W ` k ) \ _I ) )   =>    |- ( ph -> ( I + 1 ) e. ( 0..^ L ) )
Theorem	psgnunilem2 17087*	Lemma for psgnuni 17091. Induction step for moving a transposition as far to the right as possible. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
|- G = ( SymGrp ` D )   &    |- T = ran (pmTrsp ` D )   &    |- ( ph -> D e. V )   &    |- ( ph -> W e. Word T )   &    |- ( ph -> ( G gsumg W ) = ( _I |` D ) )   &    |- ( ph -> ( # ` W ) = L )   &    |- ( ph -> I e. ( 0..^ L ) )   &    |- ( ph -> A e. dom ( ( W ` I ) \ _I ) )   &    |- ( ph -> A. k e. ( 0..^ I ) -. A e. dom ( ( W ` k ) \ _I ) )   &    |- ( ph -> -. E. x e. Word T ( ( # ` x ) = ( L - 2 ) /\ ( G gsumg x ) = ( _I |` D ) ) )   =>    |- ( ph -> E. w e. Word T ( ( ( G gsumg w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( I + 1 ) e. ( 0..^ L ) /\ A e. dom ( ( w ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0..^ ( I + 1 ) ) -. A e. dom ( ( w ` j ) \ _I ) ) ) )
Theorem	psgnunilem3 17088*	Lemma for psgnuni 17091. Any nonempty representation of the identity can be incrementally transformed into a representation two shorter. (Contributed by Stefan O'Rear, 25-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- T = ran (pmTrsp ` D )   &    |- ( ph -> D e. V )   &    |- ( ph -> W e. Word T )   &    |- ( ph -> ( # ` W ) = L )   &    |- ( ph -> ( # ` W ) e. NN )   &    |- ( ph -> ( G gsumg W ) = ( _I |` D ) )   &    |- ( ph -> -. E. x e. Word T ( ( # ` x ) = ( L - 2 ) /\ ( G gsumg x ) = ( _I |` D ) ) )   =>    |- -. ph
Theorem	psgnunilem4 17089	Lemma for psgnuni 17091. An odd-length representation of the identity is impossible, as it could be repeatedly shortened to a length of 1, but a length 1 permutation must be a transposition. (Contributed by Stefan O'Rear, 25-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- T = ran (pmTrsp ` D )   &    |- ( ph -> D e. V )   &    |- ( ph -> W e. Word T )   &    |- ( ph -> ( G gsumg W ) = ( _I |` D ) )   =>    |- ( ph -> ( -u 1 ^ ( # ` W ) ) = 1 )
Theorem	m1expaddsub 17090	Addition and subtraction of parities are the same. (Contributed by Stefan O'Rear, 27-Aug-2015.)
|- ( ( X e. ZZ /\ Y e. ZZ ) -> ( -u 1 ^ ( X - Y ) ) = ( -u 1 ^ ( X + Y ) ) )
Theorem	psgnuni 17091	If the same permutation can be written in more than one way as a product of transpositions, the parity of those products must agree; otherwise the product of one with the inverse of the other would be an odd representation of the identity. (Contributed by Stefan O'Rear, 27-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- T = ran (pmTrsp ` D )   &    |- ( ph -> D e. V )   &    |- ( ph -> W e. Word T )   &    |- ( ph -> X e. Word T )   &    |- ( ph -> ( G gsumg W ) = ( G gsumg X ) )   =>    |- ( ph -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` X ) ) )
Theorem	psgnfval 17092*	Function definition of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   &    |- F = { p e. B | dom ( p \ _I ) e. Fin }   &    |- T = ran (pmTrsp ` D )   &    |- N = (pmSgn ` D )   =>    |- N = ( x e. F |-> ( iota s E. w e. Word T ( x = ( G gsumg w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
Theorem	psgnfn 17093*	Functionality and domain of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   &    |- F = { p e. B | dom ( p \ _I ) e. Fin }   &    |- N = (pmSgn ` D )   =>    |- N Fn F
Theorem	psgndmsubg 17094	The finitary permutations are a subgroup. (Contributed by Stefan O'Rear, 28-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- N = (pmSgn ` D )   =>    |- ( D e. V -> dom N e. (SubGrp ` G ) )
Theorem	psgneldm 17095	Property of being a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- N = (pmSgn ` D )   &    |- B = ( Base ` G )   =>    |- ( P e. dom N <-> ( P e. B /\ dom ( P \ _I ) e. Fin ) )
Theorem	psgneldm2 17096*	The finitary permutations are the span of the transpositions. (Contributed by Stefan O'Rear, 28-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- T = ran (pmTrsp ` D )   &    |- N = (pmSgn ` D )   =>    |- ( D e. V -> ( P e. dom N <-> E. w e. Word T P = ( G gsumg w ) ) )
Theorem	psgneldm2i 17097	A sequence of transpositions describes a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- T = ran (pmTrsp ` D )   &    |- N = (pmSgn ` D )   =>    |- ( ( D e. V /\ W e. Word T ) -> ( G gsumg W ) e. dom N )
Theorem	psgneu 17098*	A finitary permutation has exactly one parity. (Contributed by Stefan O'Rear, 28-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- T = ran (pmTrsp ` D )   &    |- N = (pmSgn ` D )   =>    |- ( P e. dom N -> E! s E. w e. Word T ( P = ( G gsumg w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
Theorem	psgnval 17099*	Value of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- T = ran (pmTrsp ` D )   &    |- N = (pmSgn ` D )   =>    |- ( P e. dom N -> ( N ` P ) = ( iota s E. w e. Word T ( P = ( G gsumg w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
Theorem	psgnvali 17100*	A finitary permutation has at least one representation for its parity. (Contributed by Stefan O'Rear, 28-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- T = ran (pmTrsp ` D )   &    |- N = (pmSgn ` D )   =>    |- ( P e. dom N -> E. w e. Word T ( P = ( G gsumg w ) /\ ( N ` P ) = ( -u 1 ^ ( # ` w ) ) ) )