Metamath Proof Explorer

Theorem psgnval

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

Ref Expression
Hypotheses psgnval.g ⊢ G = SymGrp ⁡ D
psgnval.t ⊢ T = ran ⁡ pmTrsp ⁡ D
psgnval.n ⊢ N = pmSgn ⁡ D
Assertion psgnval ⊢ P ∈ dom ⁡ N → N ⁡ P = ι s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w

Proof

Step Hyp Ref Expression
1 psgnval.g ⊢ G = SymGrp ⁡ D
2 psgnval.t ⊢ T = ran ⁡ pmTrsp ⁡ D
3 psgnval.n ⊢ N = pmSgn ⁡ D
4 eqeq1 ⊢ t = P → t = ∑ G w ↔ P = ∑ G w
5 4 anbi1d ⊢ t = P → t = ∑ G w ∧ s = − 1 w ↔ P = ∑ G w ∧ s = − 1 w
6 5 rexbidv ⊢ t = P → ∃ w ∈ Word T t = ∑ G w ∧ s = − 1 w ↔ ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w
7 6 iotabidv ⊢ t = P → ι s | ∃ w ∈ Word T t = ∑ G w ∧ s = − 1 w = ι s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w
8 eqid ⊢ Base G = Base G
9 eqid ⊢ x ∈ Base G | dom ⁡ x ∖ I ∈ Fin = x ∈ Base G | dom ⁡ x ∖ I ∈ Fin
10 1 8 9 3 psgnfn ⊢ N Fn x ∈ Base G | dom ⁡ x ∖ I ∈ Fin
11 10 fndmi ⊢ dom ⁡ N = x ∈ Base G | dom ⁡ x ∖ I ∈ Fin
12 1 8 11 2 3 psgnfval ⊢ N = t ∈ dom ⁡ N ⟼ ι s | ∃ w ∈ Word T t = ∑ G w ∧ s = − 1 w
13 iotaex ⊢ ι s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w ∈ V
14 7 12 13 fvmpt ⊢ P ∈ dom ⁡ N → N ⁡ P = ι s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w