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 = Base S
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 = Base S
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 ∈ S GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1
16 15 adantr ⊢ D ∈ Fin ∧ F ∈ P ∖ pmEven ⁡ D → N ∈ S GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1
17 14 cnmsgnbas ⊢ 1 − 1 = Base mulGrp ℂ fld ↾ 𝑠 1 − 1
18 2 17 ghmf ⊢ N ∈ S GrpHom mulGrp ℂ 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 ffvelrnd ⊢ 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