Metamath Proof Explorer

Theorem psgnfieu

Description: A permutation of a finite set has exactly one parity. (Contributed by AV, 13-Jan-2019)

Ref Expression
Hypotheses psgnfitr.g ⊢ G = SymGrp ⁡ N
psgnfitr.p ⊢ B = Base G
psgnfitr.t ⊢ T = ran ⁡ pmTrsp ⁡ N
Assertion psgnfieu ⊢ N ∈ Fin ∧ Q ∈ B → ∃! s ∃ w ∈ Word T Q = ∑ G w ∧ s = − 1 w

Proof

Step Hyp Ref Expression
1 psgnfitr.g ⊢ G = SymGrp ⁡ N
2 psgnfitr.p ⊢ B = Base G
3 psgnfitr.t ⊢ T = ran ⁡ pmTrsp ⁡ N
4 simpr ⊢ N ∈ Fin ∧ Q ∈ B → Q ∈ B
5 1 2 sygbasnfpfi ⊢ N ∈ Fin ∧ Q ∈ B → dom ⁡ Q ∖ I ∈ Fin
6 eqid ⊢ pmSgn ⁡ N = pmSgn ⁡ N
7 1 6 2 psgneldm ⊢ Q ∈ dom ⁡ pmSgn ⁡ N ↔ Q ∈ B ∧ dom ⁡ Q ∖ I ∈ Fin
8 4 5 7 sylanbrc ⊢ N ∈ Fin ∧ Q ∈ B → Q ∈ dom ⁡ pmSgn ⁡ N
9 1 3 6 psgneu ⊢ Q ∈ dom ⁡ pmSgn ⁡ N → ∃! s ∃ w ∈ Word T Q = ∑ G w ∧ s = − 1 w
10 8 9 syl ⊢ N ∈ Fin ∧ Q ∈ B → ∃! s ∃ w ∈ Word T Q = ∑ G w ∧ s = − 1 w