Theorem altgnsg

Description: The alternating group ( pmEvenD ) is a normal subgroup of the symmetric group. (Contributed by Thierry Arnoux, 18-Sep-2023)

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

Proof

Step	Hyp	Ref	Expression
1		evpmid.1	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
2		elex	$$⊢D\in \mathrm{Fin}\to D\in \mathrm{V}$$
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	2 10	syl	$$⊢D\in \mathrm{Fin}\to \mathrm{pmEven}\left(D\right)={\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]$$
12		eqid	$$⊢\mathrm{pmSgn}\left(D\right)=\mathrm{pmSgn}\left(D\right)$$
13		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
14	1 12 13	psgnghm2	$$⊢D\in \mathrm{Fin}\to \mathrm{pmSgn}\left(D\right)\in \left(S\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)$$
15		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
16		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
17	16	ringmgp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
18	15 17	ax-mp	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
19		ax-1cn	$$⊢1\in ℂ$$
20		prid1g	$$⊢1\in ℂ\to 1\in \left\{1,-1\right\}$$
21	19 20	ax-mp	$$⊢1\in \left\{1,-1\right\}$$
22		neg1cn	$$⊢-1\in ℂ$$
23		prssi	$$⊢\left(1\in ℂ\wedge -1\in ℂ\right)\to \left\{1,-1\right\}\subseteq ℂ$$
24	19 22 23	mp2an	$$⊢\left\{1,-1\right\}\subseteq ℂ$$
25		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
26	16 25	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
27		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
28	16 27	ringidval	$$⊢1=0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
29	13 26 28	ress0g	$$⊢\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}\wedge 1\in \left\{1,-1\right\}\wedge \left\{1,-1\right\}\subseteq ℂ\right)\to 1=0_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)}$$
30	18 21 24 29	mp3an	$$⊢1=0_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)}$$
31	30	ghmker	$$⊢\mathrm{pmSgn}\left(D\right)\in \left(S\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)\to {\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]\in \mathrm{NrmSGrp}\left(S\right)$$
32	14 31	syl	$$⊢D\in \mathrm{Fin}\to {\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]\in \mathrm{NrmSGrp}\left(S\right)$$
33	11 32	eqeltrd	$$⊢D\in \mathrm{Fin}\to \mathrm{pmEven}\left(D\right)\in \mathrm{NrmSGrp}\left(S\right)$$