Theorem evpmid

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

	Ref	Expression
Hypothesis	evpmid.1	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
Assertion	evpmid	$$⊢D\in \mathrm{Fin}\to {\mathrm{I}\upharpoonright }_D\in \mathrm{pmEven}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		evpmid.1	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
2	1	idresperm	$$⊢D\in \mathrm{Fin}\to {\mathrm{I}\upharpoonright }_D\in {\mathrm{Base}}_S$$
3		eqid	$$⊢\mathrm{pmSgn}\left(D\right)=\mathrm{pmSgn}\left(D\right)$$
4	3	psgnid	$$⊢D\in \mathrm{Fin}\to \mathrm{pmSgn}\left(D\right)\left({\mathrm{I}\upharpoonright }_D\right)=1$$
5		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
6	1 5 3	psgnevpmb	$$⊢D\in \mathrm{Fin}\to \left({\mathrm{I}\upharpoonright }_D\in \mathrm{pmEven}\left(D\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_D\in {\mathrm{Base}}_S\wedge \mathrm{pmSgn}\left(D\right)\left({\mathrm{I}\upharpoonright }_D\right)=1\right)\right)$$
7	2 4 6	mpbir2and	$$⊢D\in \mathrm{Fin}\to {\mathrm{I}\upharpoonright }_D\in \mathrm{pmEven}\left(D\right)$$