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 
|- S = ( SymGrp ` D )
evpmsubg.a 
|- A = ( pmEven ` D )
Assertion evpmsubg 
|- ( D e. Fin -> A e. ( SubGrp ` S ) )

Proof

Step Hyp Ref Expression
1 evpmsubg.s 
 |-  S = ( SymGrp ` D )
2 evpmsubg.a 
 |-  A = ( pmEven ` D )
3 2 evpmval 
 |-  ( D e. Fin -> A = ( `' ( pmSgn ` D ) " { 1 } ) )
4 eqid 
 |-  ( pmSgn ` D ) = ( pmSgn ` D )
5 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
6 1 4 5 psgnghm2 
 |-  ( D e. Fin -> ( pmSgn ` D ) e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
7 5 cnmsgngrp 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) e. Grp
8 5 cnmsgn0g 
 |-  1 = ( 0g ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
9 8 0subg 
 |-  ( ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) e. Grp -> { 1 } e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
10 7 9 ax-mp 
 |-  { 1 } e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
11 ghmpreima 
 |-  ( ( ( pmSgn ` D ) e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) /\ { 1 } e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) ) -> ( `' ( pmSgn ` D ) " { 1 } ) e. ( SubGrp ` S ) )
12 6 10 11 sylancl 
 |-  ( D e. Fin -> ( `' ( pmSgn ` D ) " { 1 } ) e. ( SubGrp ` S ) )
13 3 12 eqeltrd 
 |-  ( D e. Fin -> A e. ( SubGrp ` S ) )