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=BaseSymGrp⁡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=BaseSymGrp⁡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∈Wordran⁡pmTrsp⁡NQ=∑SymGrp⁡Nw∧S⁡Q=−1w
11 lencl ⊢w∈Wordran⁡pmTrsp⁡N→w∈ℕ0
12 11 nn0zd ⊢w∈Wordran⁡pmTrsp⁡N→w∈ℤ
13 m1expcl2 ⊢w∈ℤ→−1w∈−11
14 prcom ⊢−11=1−1
15 13 14 eleqtrdi ⊢w∈ℤ→−1w∈1−1
16 12 15 syl ⊢w∈Wordran⁡pmTrsp⁡N→−1w∈1−1
17 16 adantl ⊢N∈Fin∧w∈Wordran⁡pmTrsp⁡N→−1w∈1−1
18 eleq1a ⊢−1w∈1−1→S⁡Q=−1w→S⁡Q∈1−1
19 17 18 syl ⊢N∈Fin∧w∈Wordran⁡pmTrsp⁡N→S⁡Q=−1w→S⁡Q∈1−1
20 19 adantld ⊢N∈Fin∧w∈Wordran⁡pmTrsp⁡N→Q=∑SymGrp⁡Nw∧S⁡Q=−1w→S⁡Q∈1−1
21 20 rexlimdva ⊢N∈Fin→∃w∈Wordran⁡pmTrsp⁡NQ=∑SymGrp⁡Nw∧S⁡Q=−1w→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