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