Metamath Proof Explorer


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 ‘ 𝑆 ) )