Theorem psgnevpmb

Description: A class is an even permutation if it is a permutation with 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	psgnevpmb	|- ( D e. Fin -> ( F e. ( pmEven ` D ) <-> ( F e. P /\ ( 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		elex	|- ( D e. Fin -> D e. _V )
5		fveq2	|- ( d = D -> ( pmSgn ` d ) = ( pmSgn ` D ) )
6	5 3	eqtr4di	|- ( d = D -> ( pmSgn ` d ) = N )
7	6	cnveqd	|- ( d = D -> `' ( pmSgn ` d ) = `' N )
8	7	imaeq1d	|- ( d = D -> ( `' ( pmSgn ` d ) " { 1 } ) = ( `' N " { 1 } ) )
9		df-evpm	|- pmEven = ( d e. _V |-> ( `' ( pmSgn ` d ) " { 1 } ) )
10	3	fvexi	|- N e. _V
11	10	cnvex	|- `' N e. _V
12	11	imaex	|- ( `' N " { 1 } ) e. _V
13	8 9 12	fvmpt	|- ( D e. _V -> ( pmEven ` D ) = ( `' N " { 1 } ) )
14	4 13	syl	|- ( D e. Fin -> ( pmEven ` D ) = ( `' N " { 1 } ) )
15	14	eleq2d	|- ( D e. Fin -> ( F e. ( pmEven ` D ) <-> F e. ( `' N " { 1 } ) ) )
16		eqid	|- ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
17	1 3 16	psgnghm2	|- ( D e. Fin -> N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
18		eqid	|- ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) = ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
19	2 18	ghmf	|- ( N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> N : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
20	17 19	syl	|- ( D e. Fin -> N : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
21		ffn	|- ( N : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> N Fn P )
22		fniniseg	|- ( N Fn P -> ( F e. ( `' N " { 1 } ) <-> ( F e. P /\ ( N ` F ) = 1 ) ) )
23	20 21 22	3syl	|- ( D e. Fin -> ( F e. ( `' N " { 1 } ) <-> ( F e. P /\ ( N ` F ) = 1 ) ) )
24	15 23	bitrd	|- ( D e. Fin -> ( F e. ( pmEven ` D ) <-> ( F e. P /\ ( N ` F ) = 1 ) ) )