Theorem evpmid

Description: The identity is an even permutation. (Contributed by Thierry Arnoux, 18-Sep-2023)

	Ref	Expression
Hypothesis	evpmid.1	|- S = ( SymGrp ` D )
Assertion	evpmid	|- ( D e. Fin -> ( _I |` D ) e. ( pmEven ` D ) )

Proof

Step	Hyp	Ref	Expression
1		evpmid.1	|- S = ( SymGrp ` D )
2	1	idresperm	|- ( D e. Fin -> ( _I |` D ) e. ( Base ` S ) )
3		eqid	|- ( pmSgn ` D ) = ( pmSgn ` D )
4	3	psgnid	|- ( D e. Fin -> ( ( pmSgn ` D ) ` ( _I |` D ) ) = 1 )
5		eqid	|- ( Base ` S ) = ( Base ` S )
6	1 5 3	psgnevpmb	|- ( D e. Fin -> ( ( _I |` D ) e. ( pmEven ` D ) <-> ( ( _I |` D ) e. ( Base ` S ) /\ ( ( pmSgn ` D ) ` ( _I |` D ) ) = 1 ) ) )
7	2 4 6	mpbir2and	|- ( D e. Fin -> ( _I |` D ) e. ( pmEven ` D ) )