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	ffvelrnd	|- ( ( 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 )