Metamath Proof Explorer

Theorem psgnvalfi

Description: Value of the permutation sign function for permutations of finite sets. (Contributed by AV, 13-Jan-2019)

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

Proof

Step Hyp Ref Expression
1 psgnfvalfi.g ⊢ G = SymGrp ⁡ D
2 psgnfvalfi.b ⊢ B = Base G
3 psgnfvalfi.t ⊢ T = ran ⁡ pmTrsp ⁡ D
4 psgnfvalfi.n ⊢ N = pmSgn ⁡ D
5 simpr ⊢ D ∈ Fin ∧ P ∈ B → P ∈ B
6 1 2 sygbasnfpfi ⊢ D ∈ Fin ∧ P ∈ B → dom ⁡ P ∖ I ∈ Fin
7 1 4 2 psgneldm ⊢ P ∈ dom ⁡ N ↔ P ∈ B ∧ dom ⁡ P ∖ I ∈ Fin
8 5 6 7 sylanbrc ⊢ D ∈ Fin ∧ P ∈ B → P ∈ dom ⁡ N
9 1 3 4 psgnval ⊢ P ∈ dom ⁡ N → N ⁡ P = ι s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w
10 8 9 syl ⊢ D ∈ Fin ∧ P ∈ B → N ⁡ P = ι s | ∃ w ∈ Word T P = ∑ G w ∧ s = − 1 w