Metamath Proof Explorer

Theorem psgnvali

Description: A finitary permutation has at least one representation for its parity. (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 psgnvali ⊢ P ∈ dom ⁡ N → ∃ w ∈ Word T P = ∑ G w ∧ N ⁡ P = − 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 1 2 3 psgnval ⊢ P ∈ dom ⁡ N → N ⁡ P = ι s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w
5 1 2 3 psgneu ⊢ P ∈ dom ⁡ N → ∃! s ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w
6 iotacl ⊢ ∃! s ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w → ι s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w ∈ s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w
7 5 6 syl ⊢ P ∈ dom ⁡ N → ι s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w ∈ s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w
8 4 7 eqeltrd ⊢ P ∈ dom ⁡ N → N ⁡ P ∈ s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w
9 fvex ⊢ N ⁡ P ∈ V
10 eqeq1 ⊢ s = N ⁡ P → s = − 1 w ↔ N ⁡ P = − 1 w
11 10 anbi2d ⊢ s = N ⁡ P → P = ∑ G w ∧ s = − 1 w ↔ P = ∑ G w ∧ N ⁡ P = − 1 w
12 11 rexbidv ⊢ s = N ⁡ P → ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w ↔ ∃ w ∈ Word T P = ∑ G w ∧ N ⁡ P = − 1 w
13 9 12 elab ⊢ N ⁡ P ∈ s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w ↔ ∃ w ∈ Word T P = ∑ G w ∧ N ⁡ P = − 1 w
14 8 13 sylib ⊢ P ∈ dom ⁡ N → ∃ w ∈ Word T P = ∑ G w ∧ N ⁡ P = − 1 w