Theorem evpmss

Description: Even permutations are permutations. (Contributed by SO, 9-Jul-2018)

	Ref	Expression
Hypotheses	evpmss.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
	evpmss.p	$$⊢P={\mathrm{Base}}_S$$
Assertion	evpmss	$$⊢\mathrm{pmEven}\left(D\right)\subseteq P$$

Proof

Step	Hyp	Ref	Expression
1		evpmss.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
2		evpmss.p	$$⊢P={\mathrm{Base}}_S$$
3		fveq2	$$⊢d=D\to \mathrm{pmSgn}\left(d\right)=\mathrm{pmSgn}\left(D\right)$$
4	3	cnveqd	$$⊢d=D\to {\mathrm{pmSgn}\left(d\right)}^{-1}={\mathrm{pmSgn}\left(D\right)}^{-1}$$
5	4	imaeq1d	$$⊢d=D\to {\mathrm{pmSgn}\left(d\right)}^{-1}\left[\left\{1\right\}\right]={\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]$$
6		df-evpm	$$⊢\mathrm{pmEven}=\left(d\in \mathrm{V}⟼{\mathrm{pmSgn}\left(d\right)}^{-1}\left[\left\{1\right\}\right]\right)$$
7		fvex	$$⊢\mathrm{pmSgn}\left(D\right)\in \mathrm{V}$$
8	7	cnvex	$$⊢{\mathrm{pmSgn}\left(D\right)}^{-1}\in \mathrm{V}$$
9	8	imaex	$$⊢{\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]\in \mathrm{V}$$
10	5 6 9	fvmpt	$$⊢D\in \mathrm{V}\to \mathrm{pmEven}\left(D\right)={\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]$$
11		cnvimass	$$⊢{\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]\subseteq \mathrm{dom}\mathrm{pmSgn}\left(D\right)$$
12		eqid	$$⊢\mathrm{pmSgn}\left(D\right)=\mathrm{pmSgn}\left(D\right)$$
13		eqid	$$⊢S{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left(D\right)=S{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left(D\right)$$
14		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
15	1 12 13 14	psgnghm	$$⊢D\in \mathrm{V}\to \mathrm{pmSgn}\left(D\right)\in \left(\left(S{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left(D\right)\right)\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)$$
16		eqid	$$⊢{\mathrm{Base}}_{\left(S{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left(D\right)\right)}={\mathrm{Base}}_{\left(S{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left(D\right)\right)}$$
17		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)}$$
18	16 17	ghmf	$$⊢\mathrm{pmSgn}\left(D\right)\in \left(\left(S{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left(D\right)\right)\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)\to \mathrm{pmSgn}\left(D\right):{\mathrm{Base}}_{\left(S{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left(D\right)\right)}⟶{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)}$$
19		fdm	$$⊢\mathrm{pmSgn}\left(D\right):{\mathrm{Base}}_{\left(S{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left(D\right)\right)}⟶{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)}\to \mathrm{dom}\mathrm{pmSgn}\left(D\right)={\mathrm{Base}}_{\left(S{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left(D\right)\right)}$$
20	15 18 19	3syl	$$⊢D\in \mathrm{V}\to \mathrm{dom}\mathrm{pmSgn}\left(D\right)={\mathrm{Base}}_{\left(S{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left(D\right)\right)}$$
21	13 2	ressbasss	$$⊢{\mathrm{Base}}_{\left(S{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{pmSgn}\left(D\right)\right)}\subseteq P$$
22	20 21	eqsstrdi	$$⊢D\in \mathrm{V}\to \mathrm{dom}\mathrm{pmSgn}\left(D\right)\subseteq P$$
23	11 22	sstrid	$$⊢D\in \mathrm{V}\to {\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]\subseteq P$$
24	10 23	eqsstrd	$$⊢D\in \mathrm{V}\to \mathrm{pmEven}\left(D\right)\subseteq P$$
25		fvprc	$$⊢\neg D\in \mathrm{V}\to \mathrm{pmEven}\left(D\right)=\varnothing$$
26		0ss	$$⊢\varnothing \subseteq P$$
27	25 26	eqsstrdi	$$⊢\neg D\in \mathrm{V}\to \mathrm{pmEven}\left(D\right)\subseteq P$$
28	24 27	pm2.61i	$$⊢\mathrm{pmEven}\left(D\right)\subseteq P$$