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

Definition df-psgn 26738
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 26737 . 2  class pmSgn
2 vd . . 3  set  d
3 cvv 2864 . . 3  class  _V
4 vx . . . 4  set  x
5 vp . . . . . . . . 9  set  p
65cv 1641 . . . . . . . 8  class  p
7 cid 4383 . . . . . . . 8  class  _I
86, 7cdif 3225 . . . . . . 7  class  ( p 
\  _I  )
98cdm 4768 . . . . . 6  class  dom  (
p  \  _I  )
10 cfn 6948 . . . . . 6  class  Fin
119, 10wcel 1710 . . . . 5  wff  dom  (
p  \  _I  )  e.  Fin
122cv 1641 . . . . . . 7  class  d
13 csymg 14862 . . . . . . 7  class  SymGrp
1412, 13cfv 5334 . . . . . 6  class  ( SymGrp `  d )
15 cbs 13239 . . . . . 6  class  Base
1614, 15cfv 5334 . . . . 5  class  ( Base `  ( SymGrp `  d )
)
1711, 5, 16crab 2623 . . . 4  class  { p  e.  ( Base `  ( SymGrp `
 d ) )  |  dom  ( p 
\  _I  )  e. 
Fin }
184cv 1641 . . . . . . . 8  class  x
19 vw . . . . . . . . . 10  set  w
2019cv 1641 . . . . . . . . 9  class  w
21 cgsu 13494 . . . . . . . . 9  class  gsumg
2214, 20, 21co 5942 . . . . . . . 8  class  ( (
SymGrp `  d )  gsumg  w )
2318, 22wceq 1642 . . . . . . 7  wff  x  =  ( ( SymGrp `  d
)  gsumg  w )
24 vs . . . . . . . . 9  set  s
2524cv 1641 . . . . . . . 8  class  s
26 c1 8825 . . . . . . . . . 10  class  1
2726cneg 9125 . . . . . . . . 9  class  -u 1
28 chash 11427 . . . . . . . . . 10  class  #
2920, 28cfv 5334 . . . . . . . . 9  class  ( # `  w )
30 cexp 11194 . . . . . . . . 9  class  ^
3127, 29, 30co 5942 . . . . . . . 8  class  ( -u
1 ^ ( # `  w ) )
3225, 31wceq 1642 . . . . . . 7  wff  s  =  ( -u 1 ^ ( # `  w
) )
3323, 32wa 358 . . . . . 6  wff  ( x  =  ( ( SymGrp `  d )  gsumg  w )  /\  s  =  ( -u 1 ^ ( # `  w
) ) )
34 cpmtr 26707 . . . . . . . . 9  class pmTrsp
3512, 34cfv 5334 . . . . . . . 8  class  (pmTrsp `  d )
3635crn 4769 . . . . . . 7  class  ran  (pmTrsp `  d )
3736cword 11493 . . . . . 6  class Word  ran  (pmTrsp `  d )
3833, 19, 37wrex 2620 . . . . 5  wff  E. w  e. Word  ran  (pmTrsp `  d
) ( x  =  ( ( SymGrp `  d
)  gsumg  w )  /\  s  =  ( -u 1 ^ ( # `  w
) ) )
3938, 24cio 5296 . . . 4  class  ( iota s E. w  e. Word  ran  (pmTrsp `  d )
( x  =  ( ( SymGrp `  d )  gsumg  w )  /\  s  =  ( -u 1 ^ ( # `  w
) ) ) )
404, 17, 39cmpt 4156 . . 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 4156 . 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 1642 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  26746
  Copyright terms: Public domain W3C validator