Theorem evpmsubg

Description: The alternating group is a subgroup of the symmetric group. (Contributed by Thierry Arnoux, 1-Nov-2023)

	Ref	Expression
Hypotheses	evpmsubg.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
	evpmsubg.a	⊢ 𝐴 = ( pmEven ‘ 𝐷 )
Assertion	evpmsubg	⊢ ( 𝐷 ∈ Fin → 𝐴 ∈ ( SubGrp ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		evpmsubg.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2		evpmsubg.a	⊢ 𝐴 = ( pmEven ‘ 𝐷 )
3	2	evpmval	⊢ ( 𝐷 ∈ Fin → 𝐴 = ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) )
4		eqid	⊢ ( pmSgn ‘ 𝐷 ) = ( pmSgn ‘ 𝐷 )
5		eqid	⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
6	1 4 5	psgnghm2	⊢ ( 𝐷 ∈ Fin → ( pmSgn ‘ 𝐷 ) ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
7	5	cnmsgngrp	⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ∈ Grp
8	5	cnmsgn0g	⊢ 1 = ( 0g ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
9	8	0subg	⊢ ( ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ∈ Grp → { 1 } ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
10	7 9	ax-mp	⊢ { 1 } ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
11		ghmpreima	⊢ ( ( ( pmSgn ‘ 𝐷 ) ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ∧ { 1 } ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ) → ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) ∈ ( SubGrp ‘ 𝑆 ) )
12	6 10 11	sylancl	⊢ ( 𝐷 ∈ Fin → ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) ∈ ( SubGrp ‘ 𝑆 ) )
13	3 12	eqeltrd	⊢ ( 𝐷 ∈ Fin → 𝐴 ∈ ( SubGrp ‘ 𝑆 ) )