Metamath Proof Explorer

Theorem psgnfval

Description: Function definition of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgnfval.g 
|- G = ( SymGrp ` D )
psgnfval.b 
|- B = ( Base ` G )
psgnfval.f 
|- F = { p e. B | dom ( p \ _I ) e. Fin }
psgnfval.t 
|- T = ran ( pmTrsp ` D )
psgnfval.n 
|- N = ( pmSgn ` D )
Assertion psgnfval 
|- N = ( x e. F |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psgnfval.g 
 |-  G = ( SymGrp ` D )
2 psgnfval.b 
 |-  B = ( Base ` G )
3 psgnfval.f 
 |-  F = { p e. B | dom ( p \ _I ) e. Fin }
4 psgnfval.t 
 |-  T = ran ( pmTrsp ` D )
5 psgnfval.n 
 |-  N = ( pmSgn ` D )
6 fveq2 
 |-  ( d = D -> ( SymGrp ` d ) = ( SymGrp ` D ) )
7 6 1 eqtr4di 
 |-  ( d = D -> ( SymGrp ` d ) = G )
8 7 fveq2d 
 |-  ( d = D -> ( Base ` ( SymGrp ` d ) ) = ( Base ` G ) )
9 8 2 eqtr4di 
 |-  ( d = D -> ( Base ` ( SymGrp ` d ) ) = B )
10 rabeq 
 |-  ( ( Base ` ( SymGrp ` d ) ) = B -> { p e. ( Base ` ( SymGrp ` d ) ) | dom ( p \ _I ) e. Fin } = { p e. B | dom ( p \ _I ) e. Fin } )
11 9 10 syl 
 |-  ( d = D -> { p e. ( Base ` ( SymGrp ` d ) ) | dom ( p \ _I ) e. Fin } = { p e. B | dom ( p \ _I ) e. Fin } )
12 11 3 eqtr4di 
 |-  ( d = D -> { p e. ( Base ` ( SymGrp ` d ) ) | dom ( p \ _I ) e. Fin } = F )
13 fveq2 
 |-  ( d = D -> ( pmTrsp ` d ) = ( pmTrsp ` D ) )
14 13 rneqd 
 |-  ( d = D -> ran ( pmTrsp ` d ) = ran ( pmTrsp ` D ) )
15 14 4 eqtr4di 
 |-  ( d = D -> ran ( pmTrsp ` d ) = T )
16 wrdeq 
 |-  ( ran ( pmTrsp ` d ) = T -> Word ran ( pmTrsp ` d ) = Word T )
17 15 16 syl 
 |-  ( d = D -> Word ran ( pmTrsp ` d ) = Word T )
18 7 oveq1d 
 |-  ( d = D -> ( ( SymGrp ` d ) gsum w ) = ( G gsum w ) )
19 18 eqeq2d 
 |-  ( d = D -> ( x = ( ( SymGrp ` d ) gsum w ) <-> x = ( G gsum w ) ) )
20 19 anbi1d 
 |-  ( d = D -> ( ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
21 17 20 rexeqbidv 
 |-  ( d = D -> ( E. w e. Word ran ( pmTrsp ` d ) ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
22 21 iotabidv 
 |-  ( d = D -> ( iota s E. w e. Word ran ( pmTrsp ` d ) ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) = ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
23 12 22 mpteq12dv 
 |-  ( d = D -> ( 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 ) ) ) ) ) = ( x e. F |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) )
24 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 ) ) ) ) ) )
25 2 fvexi 
 |-  B e. _V
26 3 25 rabex2 
 |-  F e. _V
27 26 mptex 
 |-  ( x e. F |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) e. _V
28 23 24 27 fvmpt 
 |-  ( D e. _V -> ( pmSgn ` D ) = ( x e. F |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) )
29 fvprc 
 |-  ( -. D e. _V -> ( pmSgn ` D ) = (/) )
30 fvprc 
 |-  ( -. D e. _V -> ( SymGrp ` D ) = (/) )
31 1 30 eqtrid 
 |-  ( -. D e. _V -> G = (/) )
32 31 fveq2d 
 |-  ( -. D e. _V -> ( Base ` G ) = ( Base ` (/) ) )
33 base0 
 |-  (/) = ( Base ` (/) )
34 32 33 eqtr4di 
 |-  ( -. D e. _V -> ( Base ` G ) = (/) )
35 2 34 eqtrid 
 |-  ( -. D e. _V -> B = (/) )
36 rabeq 
 |-  ( B = (/) -> { p e. B | dom ( p \ _I ) e. Fin } = { p e. (/) | dom ( p \ _I ) e. Fin } )
37 35 36 syl 
 |-  ( -. D e. _V -> { p e. B | dom ( p \ _I ) e. Fin } = { p e. (/) | dom ( p \ _I ) e. Fin } )
38 rab0 
 |-  { p e. (/) | dom ( p \ _I ) e. Fin } = (/)
39 37 38 eqtrdi 
 |-  ( -. D e. _V -> { p e. B | dom ( p \ _I ) e. Fin } = (/) )
40 3 39 eqtrid 
 |-  ( -. D e. _V -> F = (/) )
41 40 mpteq1d 
 |-  ( -. D e. _V -> ( x e. F |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) = ( x e. (/) |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) )
42 mpt0 
 |-  ( x e. (/) |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) = (/)
43 41 42 eqtrdi 
 |-  ( -. D e. _V -> ( x e. F |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) = (/) )
44 29 43 eqtr4d 
 |-  ( -. D e. _V -> ( pmSgn ` D ) = ( x e. F |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) )
45 28 44 pm2.61i 
 |-  ( pmSgn ` D ) = ( x e. F |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
46 5 45 eqtri 
 |-  N = ( x e. F |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )