Metamath Proof Explorer

Definition df-psgn

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)

Ref Expression
Assertion 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 ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpsgn 
 |-  pmSgn
1 vd 
 |-  d
2 cvv 
 |-  _V
3 vx 
 |-  x
4 vp 
 |-  p
5 cbs 
 |-  Base
6 csymg 
 |-  SymGrp
7 1 cv 
 |-  d
8 7 6 cfv 
 |-  ( SymGrp ` d )
9 8 5 cfv 
 |-  ( Base ` ( SymGrp ` d ) )
10 4 cv 
 |-  p
11 cid 
 |-  _I
12 10 11 cdif 
 |-  ( p \ _I )
13 12 cdm 
 |-  dom ( p \ _I )
14 cfn 
 |-  Fin
15 13 14 wcel 
 |-  dom ( p \ _I ) e. Fin
16 15 4 9 crab 
 |-  { p e. ( Base ` ( SymGrp ` d ) ) | dom ( p \ _I ) e. Fin }
17 vs 
 |-  s
18 vw 
 |-  w
19 cpmtr 
 |-  pmTrsp
20 7 19 cfv 
 |-  ( pmTrsp ` d )
21 20 crn 
 |-  ran ( pmTrsp ` d )
22 21 cword 
 |-  Word ran ( pmTrsp ` d )
23 3 cv 
 |-  x
24 cgsu 
 |-  gsum
25 18 cv 
 |-  w
26 8 25 24 co 
 |-  ( ( SymGrp ` d ) gsum w )
27 23 26 wceq 
 |-  x = ( ( SymGrp ` d ) gsum w )
28 17 cv 
 |-  s
29 c1 
 |-  1
30 29 cneg 
 |-  -u 1
31 cexp 
 |-  ^
32 chash 
 |-  #
33 25 32 cfv 
 |-  ( # ` w )
34 30 33 31 co 
 |-  ( -u 1 ^ ( # ` w ) )
35 28 34 wceq 
 |-  s = ( -u 1 ^ ( # ` w ) )
36 27 35 wa 
 |-  ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) )
37 36 18 22 wrex 
 |-  E. w e. Word ran ( pmTrsp ` d ) ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) )
38 37 17 cio 
 |-  ( iota s E. w e. Word ran ( pmTrsp ` d ) ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
39 3 16 38 cmpt 
 |-  ( x e. { p e. ( Base ` ( SymGrp ` d ) ) | dom ( p \ _I ) e. Fin } |-> ( iota s E. w e. Word ran ( pmTrsp ` d ) ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
40 1 2 39 cmpt 
 |-  ( 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 ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) )
41 0 40 wceq 
 |-  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 ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) )