This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( N ` F ) = -u 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 e. ( P \ ( pmEven ` D ) ) <-> ( F e. P /\ -. F e. ( pmEven ` D ) ) )
5 simpr 
 |-  ( ( D e. Fin /\ F e. P ) -> F e. P )
6 5 a1d 
 |-  ( ( D e. Fin /\ F e. P ) -> ( ( N ` F ) = 1 -> F e. P ) )
7 6 ancrd 
 |-  ( ( D e. Fin /\ F e. P ) -> ( ( N ` F ) = 1 -> ( F e. P /\ ( N ` F ) = 1 ) ) )
8 1 2 3 psgnevpmb 
 |-  ( D e. Fin -> ( F e. ( pmEven ` D ) <-> ( F e. P /\ ( N ` F ) = 1 ) ) )
9 8 adantr 
 |-  ( ( D e. Fin /\ F e. P ) -> ( F e. ( pmEven ` D ) <-> ( F e. P /\ ( N ` F ) = 1 ) ) )
10 7 9 sylibrd 
 |-  ( ( D e. Fin /\ F e. P ) -> ( ( N ` F ) = 1 -> F e. ( pmEven ` D ) ) )
11 10 con3d 
 |-  ( ( D e. Fin /\ F e. P ) -> ( -. F e. ( pmEven ` D ) -> -. ( N ` F ) = 1 ) )
12 11 impr 
 |-  ( ( D e. Fin /\ ( F e. P /\ -. F e. ( pmEven ` D ) ) ) -> -. ( N ` F ) = 1 )
13 4 12 sylan2b 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> -. ( N ` F ) = 1 )
14 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
15 1 3 14 psgnghm2 
 |-  ( D e. Fin -> N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
16 15 adantr 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
17 14 cnmsgnbas 
 |-  { 1 , -u 1 } = ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
18 2 17 ghmf 
 |-  ( N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> N : P --> { 1 , -u 1 } )
19 16 18 syl 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> N : P --> { 1 , -u 1 } )
20 eldifi 
 |-  ( F e. ( P \ ( pmEven ` D ) ) -> F e. P )
21 20 adantl 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> F e. P )
22 19 21 ffvelcdmd 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( N ` F ) e. { 1 , -u 1 } )
23 fvex 
 |-  ( N ` F ) e. _V
24 23 elpr 
 |-  ( ( N ` F ) e. { 1 , -u 1 } <-> ( ( N ` F ) = 1 \/ ( N ` F ) = -u 1 ) )
25 22 24 sylib 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( ( N ` F ) = 1 \/ ( N ` F ) = -u 1 ) )
26 orel1 
 |-  ( -. ( N ` F ) = 1 -> ( ( ( N ` F ) = 1 \/ ( N ` F ) = -u 1 ) -> ( N ` F ) = -u 1 ) )
27 13 25 26 sylc 
 |-  ( ( D e. Fin /\ F e. ( P \ ( pmEven ` D ) ) ) -> ( N ` F ) = -u 1 )