P. 167 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16601-16700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pmtrffv 16601	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 16602*	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 16603	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 16604	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 16605	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 16606	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 16607	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 16608	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 16609*	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 16610*	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 16611	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 16612*	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 16613	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 16614	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 16615	Lemma 1 for pmtr3ncom 16617. (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 16616	Lemma 2 for pmtr3ncom 16617. (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 16617*	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 16618	Lemma 1 for pmtrdifel 16622. (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 16619	Lemma 2 for pmtrdifel 16622. (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 16620*	Lemma 3 for pmtrdifel 16622. (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 16621	Lemma 4 for pmtrdifel 16622. (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 16622*	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 16623*	Lemma 1 for pmtrdifwrdel 16627. (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 16624*	Lemma 2 for pmtrdifwrdel 16627. (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 16625*	Lemma 3 for pmtrdifwrdel 16627. (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 16626*	Lemma 1 for pmtrdifwrdel2 16628. (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 16627*	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 16628*	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 16629*	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 16630	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 16631	Syntax for the sign of a permutation.
class pmSgn
Syntax	cevpm 16632	Syntax for even permutations.
class pmEven
Definition	df-psgn 16633*	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 16634	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 16635*	Lemma for psgnuni 16641. 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 16636*	Lemma for psgnuni 16641. 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 16637*	Lemma for psgnuni 16641. 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 16638*	Lemma for psgnuni 16641. 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 16639	Lemma for psgnuni 16641. 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 16640	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 16641	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 16642*	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 16643*	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 16644	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 16645	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 16646*	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 16647	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 16648*	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 16649*	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 16650*	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 16651	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 16652	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 16653	The permutation sign function for an empty set at an empty set is 1. (Contributed by AV, 27-Feb-2019.)
|- ( (pmSgn ` (/) ) ` (/) ) = 1
Theorem	sygbasnfpfi 16654	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 16655*	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 16656*	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 16657	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 16658	The group sum of transpositions of a finite set is a permutation, see also psgneldm2i 16647. (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 )
Theorem	psgnfitr 16659*	A permutation of a finite set is generated by transpositions. (Contributed by AV, 13-Jan-2019.)
|- G = ( SymGrp ` N )   &    |- B = ( Base ` G )   &    |- T = ran (pmTrsp ` N )   =>    |- ( N e. Fin -> ( Q e. B <-> E. w e. Word T Q = ( G gsumg w ) ) )
Theorem	psgnfieu 16660*	A permutation of a finite set has exactly one parity. (Contributed by AV, 13-Jan-2019.)
|- G = ( SymGrp ` N )   &    |- B = ( Base ` G )   &    |- T = ran (pmTrsp ` N )   =>    |- ( ( N e. Fin /\ Q e. B ) -> E! s E. w e. Word T ( Q = ( G gsumg w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
Theorem	pmtrsn 16661	The value of the transposition generator function for a singleton is empty, i.e. there is no transposition for a singleton. This also holds for A e/ _V, i.e. for the empty set { A } = (/) resulting in (pmTrsp ` (/) ) = (/). (Contributed by AV, 6-Aug-2019.)
|- (pmTrsp ` { A } ) = (/)
Theorem	psgnsn 16662	The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019.)
|- D = { A }   &    |- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   &    |- N = (pmSgn ` D )   =>    |- ( ( A e. V /\ X e. B ) -> ( N ` X ) = 1 )
Theorem	psgnprfval 16663*	The permutation sign function for a pair. (Contributed by AV, 10-Dec-2018.)
|- D = { 1 , 2 }   &    |- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   &    |- T = ran (pmTrsp ` D )   &    |- N = (pmSgn ` D )   =>    |- ( X e. B -> ( N ` X ) = ( iota s E. w e. Word T ( X = ( G gsumg w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
Theorem	psgnprfval1 16664	The permutation sign of the identity for a pair. (Contributed by AV, 11-Dec-2018.)
|- D = { 1 , 2 }   &    |- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   &    |- T = ran (pmTrsp ` D )   &    |- N = (pmSgn ` D )   =>    |- ( N ` { <. 1 , 1 >. , <. 2 , 2 >. } ) = 1
Theorem	psgnprfval2 16665	The permutation sign of the transposition for a pair. (Contributed by AV, 10-Dec-2018.)
|- D = { 1 , 2 }   &    |- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   &    |- T = ran (pmTrsp ` D )   &    |- N = (pmSgn ` D )   =>    |- ( N ` { <. 1 , 2 >. , <. 2 , 1 >. } ) = -u 1
10.2.9  p-Groups and Sylow groups; Sylow's theorems
Syntax	cod 16666	Extend class notation to include the order function on the elements of a group.
class od
Syntax	cgex 16667	Extend class notation to include the order function on the elements of a group.
class gEx
Syntax	cpgp 16668	Extend class notation to include the class of all p-groups.
class pGrp
Syntax	cslw 16669	Extend class notation to include the class of all Sylow p-subgroups of a group.
class pSyl
Definition	df-od 16670*	Define the order of an element in a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.)
|- od = ( g e. _V |-> ( x e. ( Base ` g ) |-> [_ { n e. NN | ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , sup ( i , RR , `' < ) ) ) )
Definition	df-gex 16671*	Define the exponent of a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.)
|- gEx = ( g e. _V |-> [_ { n e. NN | A. x e. ( Base ` g ) ( n (.g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , sup ( i , RR , `' < ) ) )
Definition	df-pgp 16672*	Define the set of p-groups, which are groups such that every element has a power of p as its order. (Contributed by Mario Carneiro, 15-Jan-2015.)
|- pGrp = { <. p , g >. | ( ( p e. Prime /\ g e. Grp ) /\ A. x e. ( Base ` g ) E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n ) ) }
Definition	df-slw 16673*	Define the set of Sylow p-subgroups of a group g. A Sylow p-subgroup is a p-group that is not a subgroup of any other p-groups in g. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- pSyl = ( p e. Prime , g e. Grp |-> { h e. (SubGrp ` g ) | A. k e. (SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g ↾s k ) ) <-> h = k ) } )
Theorem	odfval 16674*	Value of the order function. (Contributed by Mario Carneiro, 13-Jul-2014.)
|- X = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   &    |- O = ( od ` G )   =>    |- O = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , sup ( i , RR , `' < ) ) )
Theorem	odval 16675*	Second substitution for the group order definition. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 5-Sep-2015.)
|- X = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   &    |- O = ( od ` G )   &    |- I = { y e. NN | ( y .x. A ) = .0. }   =>    |- ( A e. X -> ( O ` A ) = if ( I = (/) , 0 , sup ( I , RR , `' < ) ) )
Theorem	odlem1 16676*	The group element order is either zero or a nonzero multiplier that annihilates the element. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.)
|- X = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   &    |- O = ( od ` G )   &    |- I = { y e. NN | ( y .x. A ) = .0. }   =>    |- ( A e. X -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) )
Theorem	odcl 16677	The order of a group element is always a nonnegative integer. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   =>    |- ( A e. X -> ( O ` A ) e. NN0 )
Theorem	odf 16678	Functionality of the group element order. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   =>    |- O : X --> NN0
Theorem	odid 16679	Any element to the power of its order is the identity. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( A e. X -> ( ( O ` A ) .x. A ) = .0. )
Theorem	odlem2 16680	Any positive annihilator of a group element is an upper bound on the (positive) order of the element. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( A e. X /\ N e. NN /\ ( N .x. A ) = .0. ) -> ( O ` A ) e. ( 1 ... N ) )
Theorem	odmodnn0 16681	Reduce the argument of a group multiple by modding out the order of the element. (Contributed by Mario Carneiro, 23-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( N mod ( O ` A ) ) .x. A ) = ( N .x. A ) )
Theorem	mndodconglem 16682	Lemma for mndodcong 16683. (Contributed by Mario Carneiro, 23-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> A e. X )   &    |- ( ph -> ( O ` A ) e. NN )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> M < ( O ` A ) )   &    |- ( ph -> N < ( O ` A ) )   &    |- ( ph -> ( M .x. A ) = ( N .x. A ) )   =>    |- ( ( ph /\ M <_ N ) -> M = N )
Theorem	mndodcong 16683	If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. (Contributed by Mario Carneiro, 23-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) || ( M - N ) <-> ( M .x. A ) = ( N .x. A ) ) )
Theorem	mndodcongi 16684	If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. For monoids, the reverse implication is false for elements with infinite order. For example, the powers of 2 mod 10 are 1,2,4,8,6,2,4,8,6,... so that the identity 1 never repeats, which is infinite order by our definition, yet other numbers like 6 appear many times in the sequence. (Contributed by Mario Carneiro, 23-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) )
Theorem	oddvdsnn0 16685	The only multiples of A that are equal to the identity are the multiples of the order of A. (Contributed by Mario Carneiro, 23-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )
Theorem	odnncl 16686	If a nonzero multiple of an element is zero, the element has positive order. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( O ` A ) e. NN )
Theorem	odmod 16687	Reduce the argument of a group multiple by modding out the order of the element. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 6-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( N mod ( O ` A ) ) .x. A ) = ( N .x. A ) )
Theorem	oddvds 16688	The only multiples of A that are equal to the identity are the multiples of the order of A. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )
Theorem	oddvdsi 16689	Any group element is annihilated by any multiple of its order. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 23-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ A e. X /\ ( O ` A ) || N ) -> ( N .x. A ) = .0. )
Theorem	odcong 16690	If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ A e. X /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( O ` A ) || ( M - N ) <-> ( M .x. A ) = ( N .x. A ) ) )
Theorem	odeq 16691*	The oddvds 16688 property uniquely defines the group order. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ A e. X /\ N e. NN0 ) -> ( N = ( O ` A ) <-> A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) )
Theorem	odval2 16692*	A non-conditional definition of the group order. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ A e. X ) -> ( O ` A ) = ( iota_ x e. NN0 A. y e. NN0 ( x || y <-> ( y .x. A ) = .0. ) ) )
Theorem	odmulgid 16693	A relationship between the order of a multiple and the order of the basepoint. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( O ` ( N .x. A ) ) || K <-> ( O ` A ) || ( K x. N ) ) )
Theorem	odmulg2 16694	The order of a multiple divides the order of the base point. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` ( N .x. A ) ) || ( O ` A ) )
Theorem	odmulg 16695	Relationship between the order of an element and that of a multiple. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` A ) = ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) )
Theorem	odmulgeq 16696	A multiple of a point of finite order only has the same order if the multiplier is relatively prime. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` ( N .x. A ) ) = ( O ` A ) <-> ( N gcd ( O ` A ) ) = 1 ) )
Theorem	odbezout 16697*	If N is coprime to the order of A, there is a modular inverse x to cancel multiplication by N. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) -> E. x e. ZZ ( x .x. ( N .x. A ) ) = A )
Theorem	od1 16698	The order of the group identity is one. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.)
|- O = ( od ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> ( O ` .0. ) = 1 )
Theorem	odeq1 16699	The group identity is the unique element of a group with order one. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.)
|- O = ( od ` G )   &    |- .0. = ( 0g ` G )   &    |- X = ( Base ` G )   =>    |- ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 1 <-> A = .0. ) )
Theorem	odinv 16700	The order of the inverse of a group element. (Contributed by Mario Carneiro, 20-Oct-2015.)
|- O = ( od ` G )   &    |- I = ( invg ` G )   &    |- X = ( Base ` G )   =>    |- ( ( G e. Grp /\ A e. X ) -> ( O ` ( I ` A ) ) = ( O ` A ) )