Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-psgn Structured version   Unicode version

Definition df-psgn 27406
Description: Define a function which takes the value  1 for even permutations and  -u 1 for odd. (Contributed by Stefan O'Rear, 28-Aug-2015.)
Assertion
Ref Expression
df-psgn  |- 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
) ) ) ) ) )
Distinct variable group:    x, s, w, d, p

Detailed syntax breakdown of Definition df-psgn
StepHypRef Expression
1 cpsgn 27405 . 2  class pmSgn
2 vd . . 3  set  d
3 cvv 2958 . . 3  class  _V
4 vx . . . 4  set  x
5 vp . . . . . . . . 9  set  p
65cv 1652 . . . . . . . 8  class  p
7 cid 4496 . . . . . . . 8  class  _I
86, 7cdif 3319 . . . . . . 7  class  ( p 
\  _I  )
98cdm 4881 . . . . . 6  class  dom  (
p  \  _I  )
10 cfn 7112 . . . . . 6  class  Fin
119, 10wcel 1726 . . . . 5  wff  dom  (
p  \  _I  )  e.  Fin
122cv 1652 . . . . . . 7  class  d
13 csymg 15097 . . . . . . 7  class  SymGrp
1412, 13cfv 5457 . . . . . 6  class  ( SymGrp `  d )
15 cbs 13474 . . . . . 6  class  Base
1614, 15cfv 5457 . . . . 5  class  ( Base `  ( SymGrp `  d )
)
1711, 5, 16crab 2711 . . . 4  class  { p  e.  ( Base `  ( SymGrp `
 d ) )  |  dom  ( p 
\  _I  )  e. 
Fin }
184cv 1652 . . . . . . . 8  class  x
19 vw . . . . . . . . . 10  set  w
2019cv 1652 . . . . . . . . 9  class  w
21 cgsu 13729 . . . . . . . . 9  class  gsumg
2214, 20, 21co 6084 . . . . . . . 8  class  ( (
SymGrp `  d )  gsumg  w )
2318, 22wceq 1653 . . . . . . 7  wff  x  =  ( ( SymGrp `  d
)  gsumg  w )
24 vs . . . . . . . . 9  set  s
2524cv 1652 . . . . . . . 8  class  s
26 c1 8996 . . . . . . . . . 10  class  1
2726cneg 9297 . . . . . . . . 9  class  -u 1
28 chash 11623 . . . . . . . . . 10  class  #
2920, 28cfv 5457 . . . . . . . . 9  class  ( # `  w )
30 cexp 11387 . . . . . . . . 9  class  ^
3127, 29, 30co 6084 . . . . . . . 8  class  ( -u
1 ^ ( # `  w ) )
3225, 31wceq 1653 . . . . . . 7  wff  s  =  ( -u 1 ^ ( # `  w
) )
3323, 32wa 360 . . . . . 6  wff  ( x  =  ( ( SymGrp `  d )  gsumg  w )  /\  s  =  ( -u 1 ^ ( # `  w
) ) )
34 cpmtr 27375 . . . . . . . . 9  class pmTrsp
3512, 34cfv 5457 . . . . . . . 8  class  (pmTrsp `  d )
3635crn 4882 . . . . . . 7  class  ran  (pmTrsp `  d )
3736cword 11722 . . . . . 6  class Word  ran  (pmTrsp `  d )
3833, 19, 37wrex 2708 . . . . 5  wff  E. w  e. Word  ran  (pmTrsp `  d
) ( x  =  ( ( SymGrp `  d
)  gsumg  w )  /\  s  =  ( -u 1 ^ ( # `  w
) ) )
3938, 24cio 5419 . . . 4  class  ( iota s E. w  e. Word  ran  (pmTrsp `  d )
( x  =  ( ( SymGrp `  d )  gsumg  w )  /\  s  =  ( -u 1 ^ ( # `  w
) ) ) )
404, 17, 39cmpt 4269 . . 3  class  ( 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
) ) ) ) )
412, 3, 40cmpt 4269 . 2  class  ( 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
) ) ) ) ) )
421, 41wceq 1653 1  wff 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
) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  psgnfval  27414
  Copyright terms: Public domain W3C validator