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 ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
evpmss.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
psgnevpmb.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion psgnodpm ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ) → ( 𝑁 ‘ 𝐹 ) = - 1 )

Proof

Step Hyp Ref Expression
1 evpmss.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2 evpmss.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
3 psgnevpmb.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
4 eldif ⊢ ( 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ↔ ( 𝐹 ∈ 𝑃 ∧ ¬ 𝐹 ∈ ( pmEven ‘ 𝐷 ) ) )
5 simpr ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → 𝐹 ∈ 𝑃 )
6 5 a1d ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( ( 𝑁 ‘ 𝐹 ) = 1 → 𝐹 ∈ 𝑃 ) )
7 6 ancrd ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( ( 𝑁 ‘ 𝐹 ) = 1 → ( 𝐹 ∈ 𝑃 ∧ ( 𝑁 ‘ 𝐹 ) = 1 ) ) )
8 1 2 3 psgnevpmb ⊢ ( 𝐷 ∈ Fin → ( 𝐹 ∈ ( pmEven ‘ 𝐷 ) ↔ ( 𝐹 ∈ 𝑃 ∧ ( 𝑁 ‘ 𝐹 ) = 1 ) ) )
9 8 adantr ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( 𝐹 ∈ ( pmEven ‘ 𝐷 ) ↔ ( 𝐹 ∈ 𝑃 ∧ ( 𝑁 ‘ 𝐹 ) = 1 ) ) )
10 7 9 sylibrd ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( ( 𝑁 ‘ 𝐹 ) = 1 → 𝐹 ∈ ( pmEven ‘ 𝐷 ) ) )
11 10 con3d ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( ¬ 𝐹 ∈ ( pmEven ‘ 𝐷 ) → ¬ ( 𝑁 ‘ 𝐹 ) = 1 ) )
12 11 impr ⊢ ( ( 𝐷 ∈ Fin ∧ ( 𝐹 ∈ 𝑃 ∧ ¬ 𝐹 ∈ ( pmEven ‘ 𝐷 ) ) ) → ¬ ( 𝑁 ‘ 𝐹 ) = 1 )
13 4 12 sylan2b ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ) → ¬ ( 𝑁 ‘ 𝐹 ) = 1 )
14 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
15 1 3 14 psgnghm2 ⊢ ( 𝐷 ∈ Fin → 𝑁 ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
16 15 adantr ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ) → 𝑁 ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
17 14 cnmsgnbas ⊢ { 1 , - 1 } = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
18 2 17 ghmf ⊢ ( 𝑁 ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) → 𝑁 : 𝑃 ⟶ { 1 , - 1 } )
19 16 18 syl ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ) → 𝑁 : 𝑃 ⟶ { 1 , - 1 } )
20 eldifi ⊢ ( 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) → 𝐹 ∈ 𝑃 )
21 20 adantl ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ) → 𝐹 ∈ 𝑃 )
22 19 21 ffvelrnd ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ) → ( 𝑁 ‘ 𝐹 ) ∈ { 1 , - 1 } )
23 fvex ⊢ ( 𝑁 ‘ 𝐹 ) ∈ V
24 23 elpr ⊢ ( ( 𝑁 ‘ 𝐹 ) ∈ { 1 , - 1 } ↔ ( ( 𝑁 ‘ 𝐹 ) = 1 ∨ ( 𝑁 ‘ 𝐹 ) = - 1 ) )
25 22 24 sylib ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ) → ( ( 𝑁 ‘ 𝐹 ) = 1 ∨ ( 𝑁 ‘ 𝐹 ) = - 1 ) )
26 orel1 ⊢ ( ¬ ( 𝑁 ‘ 𝐹 ) = 1 → ( ( ( 𝑁 ‘ 𝐹 ) = 1 ∨ ( 𝑁 ‘ 𝐹 ) = - 1 ) → ( 𝑁 ‘ 𝐹 ) = - 1 ) )
27 13 25 26 sylc ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) ) → ( 𝑁 ‘ 𝐹 ) = - 1 )