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 27415
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 27414 . 2  class pmSgn
2 vd . . 3  set  d
3 cvv 2788 . . 3  class  _V
4 vx . . . 4  set  x
5 vp . . . . . . . . 9  set  p
65cv 1622 . . . . . . . 8  class  p
7 cid 4304 . . . . . . . 8  class  _I
86, 7cdif 3149 . . . . . . 7  class  ( p 
\  _I  )
98cdm 4689 . . . . . 6  class  dom  (
p  \  _I  )
10 cfn 6863 . . . . . 6  class  Fin
119, 10wcel 1684 . . . . 5  wff  dom  (
p  \  _I  )  e.  Fin
122cv 1622 . . . . . . 7  class  d
13 csymg 14769 . . . . . . 7  class  SymGrp
1412, 13cfv 5255 . . . . . 6  class  ( SymGrp `  d )
15 cbs 13148 . . . . . 6  class  Base
1614, 15cfv 5255 . . . . 5  class  ( Base `  ( SymGrp `  d )
)
1711, 5, 16crab 2547 . . . 4  class  { p  e.  ( Base `  ( SymGrp `
 d ) )  |  dom  ( p 
\  _I  )  e. 
Fin }
184cv 1622 . . . . . . . 8  class  x
19 vw . . . . . . . . . 10  set  w
2019cv 1622 . . . . . . . . 9  class  w
21 cgsu 13401 . . . . . . . . 9  class  gsumg
2214, 20, 21co 5858 . . . . . . . 8  class  ( (
SymGrp `  d )  gsumg  w )
2318, 22wceq 1623 . . . . . . 7  wff  x  =  ( ( SymGrp `  d
)  gsumg  w )
24 vs . . . . . . . . 9  set  s
2524cv 1622 . . . . . . . 8  class  s
26 c1 8738 . . . . . . . . . 10  class  1
2726cneg 9038 . . . . . . . . 9  class  -u 1
28 chash 11337 . . . . . . . . . 10  class  #
2920, 28cfv 5255 . . . . . . . . 9  class  ( # `  w )
30 cexp 11104 . . . . . . . . 9  class  ^
3127, 29, 30co 5858 . . . . . . . 8  class  ( -u
1 ^ ( # `  w ) )
3225, 31wceq 1623 . . . . . . 7  wff  s  =  ( -u 1 ^ ( # `  w
) )
3323, 32wa 358 . . . . . 6  wff  ( x  =  ( ( SymGrp `  d )  gsumg  w )  /\  s  =  ( -u 1 ^ ( # `  w
) ) )
34 cpmtr 27384 . . . . . . . . 9  class pmTrsp
3512, 34cfv 5255 . . . . . . . 8  class  (pmTrsp `  d )
3635crn 4690 . . . . . . 7  class  ran  (pmTrsp `  d )
3736cword 11403 . . . . . 6  class Word  ran  (pmTrsp `  d )
3833, 19, 37wrex 2544 . . . . 5  wff  E. w  e. Word  ran  (pmTrsp `  d
) ( x  =  ( ( SymGrp `  d
)  gsumg  w )  /\  s  =  ( -u 1 ^ ( # `  w
) ) )
3938, 24cio 5217 . . . 4  class  ( iota s E. w  e. Word  ran  (pmTrsp `  d )
( x  =  ( ( SymGrp `  d )  gsumg  w )  /\  s  =  ( -u 1 ^ ( # `  w
) ) ) )
404, 17, 39cmpt 4077 . . 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 4077 . 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 1623 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  27423
  Copyright terms: Public domain W3C validator