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	symgextf 17001*	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 17002*	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 17003*	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 17004*	Lemma for symgextf1 17005. (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 17005*	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 17006*	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 17007*	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 17008*	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 17009*	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 17010	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 17011*	Lemma 1 for gsmsymgrfix 17012. (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 17012*	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 17013*	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 17014*	Lemma 1 for gsmsymgreq 17016. (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 17015*	Lemma 2 for gsmsymgreq 17016. (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 17016*	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 17017*	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 17018*	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 17019*	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 17020*	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 17021*	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 17022*	Lemma 1 for symgfixfo 17023. (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 17023*	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 17024*	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 17026.
Syntax	cpmtr 17025	Syntax for the transposition generator function.
class pmTrsp
Definition	df-pmtr 17026*	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 17027	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 17028	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 17029	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 17030	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 17031	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 17032	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 17033	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 17034*	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 17035*	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 17036	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 17037	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 17038	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 17039	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 17040	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 17041	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 17042	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 17043	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 17044*	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 17045	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 17046	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 17047	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 17048	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 17049	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 17050	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 17051*	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 17052*	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 17053	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 17054*	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 17055	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 17056	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 17057	Lemma 1 for pmtr3ncom 17059. (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 17058	Lemma 2 for pmtr3ncom 17059. (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 17059*	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 17060	Lemma 1 for pmtrdifel 17064. (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 17061	Lemma 2 for pmtrdifel 17064. (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 17062*	Lemma 3 for pmtrdifel 17064. (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 17063	Lemma 4 for pmtrdifel 17064. (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 17064*	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 17065*	Lemma 1 for pmtrdifwrdel 17069. (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 17066*	Lemma 2 for pmtrdifwrdel 17069. (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 17067*	Lemma 3 for pmtrdifwrdel 17069. (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 17068*	Lemma 1 for pmtrdifwrdel2 17070. (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 17069*	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 17070*	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 17071*	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 17072	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 17073	Syntax for the sign of a permutation.
class pmSgn
Syntax	cevpm 17074	Syntax for even permutations.
class pmEven
Definition	df-psgn 17075*	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 17076	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 17077*	Lemma for psgnuni 17083. 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 17078*	Lemma for psgnuni 17083. 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 17079*	Lemma for psgnuni 17083. 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 17080*	Lemma for psgnuni 17083. 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 17081	Lemma for psgnuni 17083. 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 17082	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 17083	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 17084*	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 17085*	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 17086	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 17087	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 17088*	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 17089	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 17090*	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 17091*	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 17092*	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 ) ) ) )
Theorem	psgnvalii 17093	Any representation of a permutation is length matching the permutation sign. (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 ) -> ( N ` ( G gsumg W ) ) = ( -u 1 ^ ( # ` W ) ) )
Theorem	psgnpmtr 17094	All transpositions are odd. (Contributed by Stefan O'Rear, 29-Aug-2015.)
|- G = ( SymGrp ` D )   &    |- T = ran (pmTrsp ` D )   &    |- N = (pmSgn ` D )   =>    |- ( P e. T -> ( N ` P ) = -u 1 )
Theorem	psgn0fv0 17095	The permutation sign function for an empty set at an empty set is 1. (Contributed by AV, 27-Feb-2019.)
|- ( (pmSgn ` (/) ) ` (/) ) = 1
Theorem	sygbasnfpfi 17096	The class of non-fixed points of a permutation of a finite set is finite. (Contributed by AV, 13-Jan-2019.)
|- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   =>    |- ( ( D e. Fin /\ P e. B ) -> dom ( P \ _I ) e. Fin )
Theorem	psgnfvalfi 17097*	Function definition of the permutation sign function for permutations of finite sets. (Contributed by AV, 13-Jan-2019.)
|- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   &    |- T = ran (pmTrsp ` D )   &    |- N = (pmSgn ` D )   =>    |- ( D e. Fin -> N = ( x e. B |-> ( iota s E. w e. Word T ( x = ( G gsumg w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) )
Theorem	psgnvalfi 17098*	Value of the permutation sign function for permutations of finite sets. (Contributed by AV, 13-Jan-2019.)
|- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   &    |- T = ran (pmTrsp ` D )   &    |- N = (pmSgn ` D )   =>    |- ( ( D e. Fin /\ P e. B ) -> ( N ` P ) = ( iota s E. w e. Word T ( P = ( G gsumg w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
Theorem	psgnran 17099	The range of the permutation sign function for finite permutations. (Contributed by AV, 1-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- S = (pmSgn ` N )   =>    |- ( ( N e. Fin /\ Q e. P ) -> ( S ` Q ) e. { 1 , -u 1 } )
Theorem	gsmtrcl 17100	The group sum of transpositions of a finite set is a permutation, see also psgneldm2i 17089. (Contributed by AV, 19-Jan-2019.)
|- S = ( SymGrp ` N )   &    |- B = ( Base ` S )   &    |- T = ran (pmTrsp ` N )   =>    |- ( ( N e. Fin /\ W e. Word T ) -> ( S gsumg W ) e. B )