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	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
Assertion	altgnsg	⊢ ( 𝐷 ∈ Fin → ( pmEven ‘ 𝐷 ) ∈ ( NrmSGrp ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		evpmid.1	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2		elex	⊢ ( 𝐷 ∈ Fin → 𝐷 ∈ V )
3		fveq2	⊢ ( 𝑑 = 𝐷 → ( pmSgn ‘ 𝑑 ) = ( pmSgn ‘ 𝐷 ) )
4	3	cnveqd	⊢ ( 𝑑 = 𝐷 → ◡ ( pmSgn ‘ 𝑑 ) = ◡ ( pmSgn ‘ 𝐷 ) )
5	4	imaeq1d	⊢ ( 𝑑 = 𝐷 → ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) = ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) )
6		df-evpm	⊢ pmEven = ( 𝑑 ∈ V ↦ ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) )
7		fvex	⊢ ( pmSgn ‘ 𝐷 ) ∈ V
8	7	cnvex	⊢ ◡ ( pmSgn ‘ 𝐷 ) ∈ V
9	8	imaex	⊢ ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) ∈ V
10	5 6 9	fvmpt	⊢ ( 𝐷 ∈ V → ( pmEven ‘ 𝐷 ) = ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) )
11	2 10	syl	⊢ ( 𝐷 ∈ Fin → ( pmEven ‘ 𝐷 ) = ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) )
12		eqid	⊢ ( pmSgn ‘ 𝐷 ) = ( pmSgn ‘ 𝐷 )
13		eqid	⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
14	1 12 13	psgnghm2	⊢ ( 𝐷 ∈ Fin → ( pmSgn ‘ 𝐷 ) ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
15		cnring	⊢ ℂfld ∈ Ring
16		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
17	16	ringmgp	⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
18	15 17	ax-mp	⊢ ( mulGrp ‘ ℂfld ) ∈ Mnd
19		ax-1cn	⊢ 1 ∈ ℂ
20		prid1g	⊢ ( 1 ∈ ℂ → 1 ∈ { 1 , - 1 } )
21	19 20	ax-mp	⊢ 1 ∈ { 1 , - 1 }
22		neg1cn	⊢ - 1 ∈ ℂ
23		prssi	⊢ ( ( 1 ∈ ℂ ∧ - 1 ∈ ℂ ) → { 1 , - 1 } ⊆ ℂ )
24	19 22 23	mp2an	⊢ { 1 , - 1 } ⊆ ℂ
25		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
26	16 25	mgpbas	⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
27		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
28	16 27	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
29	13 26 28	ress0g	⊢ ( ( ( mulGrp ‘ ℂfld ) ∈ Mnd ∧ 1 ∈ { 1 , - 1 } ∧ { 1 , - 1 } ⊆ ℂ ) → 1 = ( 0g ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
30	18 21 24 29	mp3an	⊢ 1 = ( 0g ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
31	30	ghmker	⊢ ( ( pmSgn ‘ 𝐷 ) ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) → ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) ∈ ( NrmSGrp ‘ 𝑆 ) )
32	14 31	syl	⊢ ( 𝐷 ∈ Fin → ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) ∈ ( NrmSGrp ‘ 𝑆 ) )
33	11 32	eqeltrd	⊢ ( 𝐷 ∈ Fin → ( pmEven ‘ 𝐷 ) ∈ ( NrmSGrp ‘ 𝑆 ) )