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=BaseG
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∈WordTx=∑Gw∧s=−1w

Proof

Step Hyp Ref Expression
1 psgnfval.g ⊢G=SymGrp⁡D
2 psgnfval.b ⊢B=BaseG
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→BaseSymGrp⁡d=BaseG
9 8 2 eqtr4di ⊢d=D→BaseSymGrp⁡d=B
10 rabeq ⊢BaseSymGrp⁡d=B→p∈BaseSymGrp⁡d|dom⁡p∖I∈Fin=p∈B|dom⁡p∖I∈Fin
11 9 10 syl ⊢d=D→p∈BaseSymGrp⁡d|dom⁡p∖I∈Fin=p∈B|dom⁡p∖I∈Fin
12 11 3 eqtr4di ⊢d=D→p∈BaseSymGrp⁡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→Wordran⁡pmTrsp⁡d=WordT
17 15 16 syl ⊢d=D→Wordran⁡pmTrsp⁡d=WordT
18 7 oveq1d ⊢d=D→∑SymGrp⁡dw=∑Gw
19 18 eqeq2d ⊢d=D→x=∑SymGrp⁡dw↔x=∑Gw
20 19 anbi1d ⊢d=D→x=∑SymGrp⁡dw∧s=−1w↔x=∑Gw∧s=−1w
21 17 20 rexeqbidv ⊢d=D→∃w∈Wordran⁡pmTrsp⁡dx=∑SymGrp⁡dw∧s=−1w↔∃w∈WordTx=∑Gw∧s=−1w
22 21 iotabidv ⊢d=D→ιs|∃w∈Wordran⁡pmTrsp⁡dx=∑SymGrp⁡dw∧s=−1w=ιs|∃w∈WordTx=∑Gw∧s=−1w
23 12 22 mpteq12dv ⊢d=D→x∈p∈BaseSymGrp⁡d|dom⁡p∖I∈Fin⟼ιs|∃w∈Wordran⁡pmTrsp⁡dx=∑SymGrp⁡dw∧s=−1w=x∈F⟼ιs|∃w∈WordTx=∑Gw∧s=−1w
24 df-psgn ⊢pmSgn=d∈V⟼x∈p∈BaseSymGrp⁡d|dom⁡p∖I∈Fin⟼ιs|∃w∈Wordran⁡pmTrsp⁡dx=∑SymGrp⁡dw∧s=−1w
25 2 fvexi ⊢B∈V
26 3 25 rabex2 ⊢F∈V
27 26 mptex ⊢x∈F⟼ιs|∃w∈WordTx=∑Gw∧s=−1w∈V
28 23 24 27 fvmpt ⊢D∈V→pmSgn⁡D=x∈F⟼ιs|∃w∈WordTx=∑Gw∧s=−1w
29 fvprc ⊢¬D∈V→pmSgn⁡D=∅
30 fvprc ⊢¬D∈V→SymGrp⁡D=∅
31 1 30 eqtrid ⊢¬D∈V→G=∅
32 31 fveq2d ⊢¬D∈V→BaseG=Base∅
33 base0 ⊢∅=Base∅
34 32 33 eqtr4di ⊢¬D∈V→BaseG=∅
35 2 34 eqtrid ⊢¬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 eqtrid ⊢¬D∈V→F=∅
41 40 mpteq1d ⊢¬D∈V→x∈F⟼ιs|∃w∈WordTx=∑Gw∧s=−1w=x∈∅⟼ιs|∃w∈WordTx=∑Gw∧s=−1w
42 mpt0 ⊢x∈∅⟼ιs|∃w∈WordTx=∑Gw∧s=−1w=∅
43 41 42 eqtrdi ⊢¬D∈V→x∈F⟼ιs|∃w∈WordTx=∑Gw∧s=−1w=∅
44 29 43 eqtr4d ⊢¬D∈V→pmSgn⁡D=x∈F⟼ιs|∃w∈WordTx=∑Gw∧s=−1w
45 28 44 pm2.61i ⊢pmSgn⁡D=x∈F⟼ιs|∃w∈WordTx=∑Gw∧s=−1w
46 5 45 eqtri ⊢N=x∈F⟼ιs|∃w∈WordTx=∑Gw∧s=−1w