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=\mathrm{SymGrp}\left(D\right)$$
	evpmss.p	$$⊢P={\mathrm{Base}}_S$$
	psgnevpmb.n	$$⊢N=\mathrm{pmSgn}\left(D\right)$$
Assertion	psgnevpmb	$$⊢D\in \mathrm{Fin}\to \left(F\in \mathrm{pmEven}\left(D\right)\leftrightarrow \left(F\in P\wedge N\left(F\right)=1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		evpmss.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
2		evpmss.p	$$⊢P={\mathrm{Base}}_S$$
3		psgnevpmb.n	$$⊢N=\mathrm{pmSgn}\left(D\right)$$
4		elex	$$⊢D\in \mathrm{Fin}\to D\in \mathrm{V}$$
5		fveq2	$$⊢d=D\to \mathrm{pmSgn}\left(d\right)=\mathrm{pmSgn}\left(D\right)$$
6	5 3	eqtr4di	$$⊢d=D\to \mathrm{pmSgn}\left(d\right)=N$$
7	6	cnveqd	$$⊢d=D\to {\mathrm{pmSgn}\left(d\right)}^{-1}=N^{-1}$$
8	7	imaeq1d	$$⊢d=D\to {\mathrm{pmSgn}\left(d\right)}^{-1}\left[\left\{1\right\}\right]=N^{-1}\left[\left\{1\right\}\right]$$
9		df-evpm	$$⊢\mathrm{pmEven}=\left(d\in \mathrm{V}⟼{\mathrm{pmSgn}\left(d\right)}^{-1}\left[\left\{1\right\}\right]\right)$$
10	3	fvexi	$$⊢N\in \mathrm{V}$$
11	10	cnvex	$$⊢N^{-1}\in \mathrm{V}$$
12	11	imaex	$$⊢N^{-1}\left[\left\{1\right\}\right]\in \mathrm{V}$$
13	8 9 12	fvmpt	$$⊢D\in \mathrm{V}\to \mathrm{pmEven}\left(D\right)=N^{-1}\left[\left\{1\right\}\right]$$
14	4 13	syl	$$⊢D\in \mathrm{Fin}\to \mathrm{pmEven}\left(D\right)=N^{-1}\left[\left\{1\right\}\right]$$
15	14	eleq2d	$$⊢D\in \mathrm{Fin}\to \left(F\in \mathrm{pmEven}\left(D\right)\leftrightarrow F\in N^{-1}\left[\left\{1\right\}\right]\right)$$
16		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
17	1 3 16	psgnghm2	$$⊢D\in \mathrm{Fin}\to N\in \left(S\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)$$
18		eqid	$$⊢{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)}$$
19	2 18	ghmf	$$⊢N\in \left(S\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)\to N:P⟶{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)}$$
20	17 19	syl	$$⊢D\in \mathrm{Fin}\to N:P⟶{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)}$$
21		ffn	$$⊢N:P⟶{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)}\to NFnP$$
22		fniniseg	$$⊢NFnP\to \left(F\in N^{-1}\left[\left\{1\right\}\right]\leftrightarrow \left(F\in P\wedge N\left(F\right)=1\right)\right)$$
23	20 21 22	3syl	$$⊢D\in \mathrm{Fin}\to \left(F\in N^{-1}\left[\left\{1\right\}\right]\leftrightarrow \left(F\in P\wedge N\left(F\right)=1\right)\right)$$
24	15 23	bitrd	$$⊢D\in \mathrm{Fin}\to \left(F\in \mathrm{pmEven}\left(D\right)\leftrightarrow \left(F\in P\wedge N\left(F\right)=1\right)\right)$$