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 B | dom p I Fin
psgnfval.t T = ran pmTrsp D
psgnfval.n N = pmSgn D
Assertion psgnfval N = x F ι s | w Word T x = G w s = 1 w

Proof

Step Hyp Ref Expression
1 psgnfval.g G = SymGrp D
2 psgnfval.b B = Base G
3 psgnfval.f F = p B | dom p I 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 Base SymGrp d | dom p I Fin = p B | dom p I Fin
11 9 10 syl d = D p Base SymGrp d | dom p I Fin = p B | dom p I Fin
12 11 3 eqtr4di d = D p Base SymGrp d | dom p I 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 w = G w
19 18 eqeq2d d = D x = SymGrp d w x = G w
20 19 anbi1d d = D x = SymGrp d w s = 1 w x = G w s = 1 w
21 17 20 rexeqbidv d = D w Word ran pmTrsp d x = SymGrp d w s = 1 w w Word T x = G w s = 1 w
22 21 iotabidv d = D ι s | w Word ran pmTrsp d x = SymGrp d w s = 1 w = ι s | w Word T x = G w s = 1 w
23 12 22 mpteq12dv d = D x p Base SymGrp d | dom p I Fin ι s | w Word ran pmTrsp d x = SymGrp d w s = 1 w = x F ι s | w Word T x = G w s = 1 w
24 df-psgn pmSgn = d V x p Base SymGrp d | dom p I Fin ι s | w Word ran pmTrsp d x = SymGrp d w s = 1 w
25 2 fvexi B V
26 3 25 rabex2 F V
27 26 mptex x F ι s | w Word T x = G w s = 1 w V
28 23 24 27 fvmpt D V pmSgn D = x F ι s | w Word T x = G w s = 1 w
29 fvprc ¬ D V pmSgn D =
30 fvprc ¬ D V SymGrp D =
31 1 30 syl5eq ¬ D V G =
32 31 fveq2d ¬ D V Base G = Base
33 base0 = Base
34 32 33 eqtr4di ¬ D V Base G =
35 2 34 syl5eq ¬ D V B =
36 rabeq B = p B | dom p I Fin = p | dom p I Fin
37 35 36 syl ¬ D V p B | dom p I Fin = p | dom p I Fin
38 rab0 p | dom p I Fin =
39 37 38 eqtrdi ¬ D V p B | dom p I Fin =
40 3 39 syl5eq ¬ D V F =
41 40 mpteq1d ¬ D V x F ι s | w Word T x = G w s = 1 w = x ι s | w Word T x = G w s = 1 w
42 mpt0 x ι s | w Word T x = G w s = 1 w =
43 41 42 eqtrdi ¬ D V x F ι s | w Word T x = G w s = 1 w =
44 29 43 eqtr4d ¬ D V pmSgn D = x F ι s | w Word T x = G w s = 1 w
45 28 44 pm2.61i pmSgn D = x F ι s | w Word T x = G w s = 1 w
46 5 45 eqtri N = x F ι s | w Word T x = G w s = 1 w