Metamath Proof Explorer

Theorem psgnodpm

Description: A permutation which is odd (i.e. not even) has sign -1. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses evpmss.s ⊢S=SymGrp⁡D
evpmss.p ⊢P=BaseS
psgnevpmb.n ⊢N=pmSgn⁡D
Assertion psgnodpm ⊢D∈Fin∧F∈P∖pmEven⁡D→N⁡F=−1

Proof

Step Hyp Ref Expression
1 evpmss.s ⊢S=SymGrp⁡D
2 evpmss.p ⊢P=BaseS
3 psgnevpmb.n ⊢N=pmSgn⁡D
4 eldif ⊢F∈P∖pmEven⁡D↔F∈P∧¬F∈pmEven⁡D
5 simpr ⊢D∈Fin∧F∈P→F∈P
6 5 a1d ⊢D∈Fin∧F∈P→N⁡F=1→F∈P
7 6 ancrd ⊢D∈Fin∧F∈P→N⁡F=1→F∈P∧N⁡F=1
8 1 2 3 psgnevpmb ⊢D∈Fin→F∈pmEven⁡D↔F∈P∧N⁡F=1
9 8 adantr ⊢D∈Fin∧F∈P→F∈pmEven⁡D↔F∈P∧N⁡F=1
10 7 9 sylibrd ⊢D∈Fin∧F∈P→N⁡F=1→F∈pmEven⁡D
11 10 con3d ⊢D∈Fin∧F∈P→¬F∈pmEven⁡D→¬N⁡F=1
12 11 impr ⊢D∈Fin∧F∈P∧¬F∈pmEven⁡D→¬N⁡F=1
13 4 12 sylan2b ⊢D∈Fin∧F∈P∖pmEven⁡D→¬N⁡F=1
14 eqid ⊢mulGrpℂfld↾𝑠1−1=mulGrpℂfld↾𝑠1−1
15 1 3 14 psgnghm2 ⊢D∈Fin→N∈SGrpHommulGrpℂfld↾𝑠1−1
16 15 adantr ⊢D∈Fin∧F∈P∖pmEven⁡D→N∈SGrpHommulGrpℂfld↾𝑠1−1
17 14 cnmsgnbas ⊢1−1=BasemulGrpℂfld↾𝑠1−1
18 2 17 ghmf ⊢N∈SGrpHommulGrpℂfld↾𝑠1−1→N:P⟶1−1
19 16 18 syl ⊢D∈Fin∧F∈P∖pmEven⁡D→N:P⟶1−1
20 eldifi ⊢F∈P∖pmEven⁡D→F∈P
21 20 adantl ⊢D∈Fin∧F∈P∖pmEven⁡D→F∈P
22 19 21 ffvelcdmd ⊢D∈Fin∧F∈P∖pmEven⁡D→N⁡F∈1−1
23 fvex ⊢N⁡F∈V
24 23 elpr ⊢N⁡F∈1−1↔N⁡F=1∨N⁡F=−1
25 22 24 sylib ⊢D∈Fin∧F∈P∖pmEven⁡D→N⁡F=1∨N⁡F=−1
26 orel1 ⊢¬N⁡F=1→N⁡F=1∨N⁡F=−1→N⁡F=−1
27 13 25 26 sylc ⊢D∈Fin∧F∈P∖pmEven⁡D→N⁡F=−1