Metamath Proof Explorer

Theorem psgnran

Description: The range of the permutation sign function for finite permutations. (Contributed by AV, 1-Jan-2019)

Ref Expression
Hypotheses psgnran.p ⊢ P = Base SymGrp ⁡ N
psgnran.s ⊢ S = pmSgn ⁡ N
Assertion psgnran ⊢ N ∈ Fin ∧ Q ∈ P → S ⁡ Q ∈ 1 − 1

Proof

Step Hyp Ref Expression
1 psgnran.p ⊢ P = Base SymGrp ⁡ N
2 psgnran.s ⊢ S = pmSgn ⁡ N
3 eqid ⊢ SymGrp ⁡ N = SymGrp ⁡ N
4 3 1 sygbasnfpfi ⊢ N ∈ Fin ∧ Q ∈ P → dom ⁡ Q ∖ I ∈ Fin
5 4 ex ⊢ N ∈ Fin → Q ∈ P → dom ⁡ Q ∖ I ∈ Fin
6 5 pm4.71d ⊢ N ∈ Fin → Q ∈ P ↔ Q ∈ P ∧ dom ⁡ Q ∖ I ∈ Fin
7 3 2 1 psgneldm ⊢ Q ∈ dom ⁡ S ↔ Q ∈ P ∧ dom ⁡ Q ∖ I ∈ Fin
8 6 7 bitr4di ⊢ N ∈ Fin → Q ∈ P ↔ Q ∈ dom ⁡ S
9 eqid ⊢ ran ⁡ pmTrsp ⁡ N = ran ⁡ pmTrsp ⁡ N
10 3 9 2 psgnvali ⊢ Q ∈ dom ⁡ S → ∃ w ∈ Word ran ⁡ pmTrsp ⁡ N Q = ∑ SymGrp ⁡ N w ∧ S ⁡ Q = − 1 w
11 lencl ⊢ w ∈ Word ran ⁡ pmTrsp ⁡ N → w ∈ ℕ 0
12 11 nn0zd ⊢ w ∈ Word ran ⁡ pmTrsp ⁡ N → w ∈ ℤ
13 m1expcl2 ⊢ w ∈ ℤ → − 1 w ∈ − 1 1
14 prcom ⊢ − 1 1 = 1 − 1
15 13 14 eleqtrdi ⊢ w ∈ ℤ → − 1 w ∈ 1 − 1
16 12 15 syl ⊢ w ∈ Word ran ⁡ pmTrsp ⁡ N → − 1 w ∈ 1 − 1
17 16 adantl ⊢ N ∈ Fin ∧ w ∈ Word ran ⁡ pmTrsp ⁡ N → − 1 w ∈ 1 − 1
18 eleq1a ⊢ − 1 w ∈ 1 − 1 → S ⁡ Q = − 1 w → S ⁡ Q ∈ 1 − 1
19 17 18 syl ⊢ N ∈ Fin ∧ w ∈ Word ran ⁡ pmTrsp ⁡ N → S ⁡ Q = − 1 w → S ⁡ Q ∈ 1 − 1
20 19 adantld ⊢ N ∈ Fin ∧ w ∈ Word ran ⁡ pmTrsp ⁡ N → Q = ∑ SymGrp ⁡ N w ∧ S ⁡ Q = − 1 w → S ⁡ Q ∈ 1 − 1
21 20 rexlimdva ⊢ N ∈ Fin → ∃ w ∈ Word ran ⁡ pmTrsp ⁡ N Q = ∑ SymGrp ⁡ N w ∧ S ⁡ Q = − 1 w → S ⁡ Q ∈ 1 − 1
22 10 21 syl5 ⊢ N ∈ Fin → Q ∈ dom ⁡ S → S ⁡ Q ∈ 1 − 1
23 8 22 sylbid ⊢ N ∈ Fin → Q ∈ P → S ⁡ Q ∈ 1 − 1
24 23 imp ⊢ N ∈ Fin ∧ Q ∈ P → S ⁡ Q ∈ 1 − 1