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 ) ) ) ) ) )