Metamath Proof Explorer

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 = ( SymGrp ` D )
Assertion altgnsg 
|- ( D e. Fin -> ( pmEven ` D ) e. ( NrmSGrp ` S ) )

Proof

Step Hyp Ref Expression
1 evpmid.1 
 |-  S = ( SymGrp ` D )
2 elex 
 |-  ( D e. Fin -> D e. _V )
3 fveq2 
 |-  ( d = D -> ( pmSgn ` d ) = ( pmSgn ` D ) )
4 3 cnveqd 
 |-  ( d = D -> `' ( pmSgn ` d ) = `' ( pmSgn ` D ) )
5 4 imaeq1d 
 |-  ( d = D -> ( `' ( pmSgn ` d ) " { 1 } ) = ( `' ( pmSgn ` D ) " { 1 } ) )
6 df-evpm 
 |-  pmEven = ( d e. _V |-> ( `' ( pmSgn ` d ) " { 1 } ) )
7 fvex 
 |-  ( pmSgn ` D ) e. _V
8 7 cnvex 
 |-  `' ( pmSgn ` D ) e. _V
9 8 imaex 
 |-  ( `' ( pmSgn ` D ) " { 1 } ) e. _V
10 5 6 9 fvmpt 
 |-  ( D e. _V -> ( pmEven ` D ) = ( `' ( pmSgn ` D ) " { 1 } ) )
11 2 10 syl 
 |-  ( D e. Fin -> ( pmEven ` D ) = ( `' ( pmSgn ` D ) " { 1 } ) )
12 eqid 
 |-  ( pmSgn ` D ) = ( pmSgn ` D )
13 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
14 1 12 13 psgnghm2 
 |-  ( D e. Fin -> ( pmSgn ` D ) e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
15 cnring 
 |-  CCfld e. Ring
16 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
17 16 ringmgp 
 |-  ( CCfld e. Ring -> ( mulGrp ` CCfld ) e. Mnd )
18 15 17 ax-mp 
 |-  ( mulGrp ` CCfld ) e. Mnd
19 ax-1cn 
 |-  1 e. CC
20 prid1g 
 |-  ( 1 e. CC -> 1 e. { 1 , -u 1 } )
21 19 20 ax-mp 
 |-  1 e. { 1 , -u 1 }
22 neg1cn 
 |-  -u 1 e. CC
23 prssi 
 |-  ( ( 1 e. CC /\ -u 1 e. CC ) -> { 1 , -u 1 } C_ CC )
24 19 22 23 mp2an 
 |-  { 1 , -u 1 } C_ CC
25 cnfldbas 
 |-  CC = ( Base ` CCfld )
26 16 25 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
27 cnfld1 
 |-  1 = ( 1r ` CCfld )
28 16 27 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
29 13 26 28 ress0g 
 |-  ( ( ( mulGrp ` CCfld ) e. Mnd /\ 1 e. { 1 , -u 1 } /\ { 1 , -u 1 } C_ CC ) -> 1 = ( 0g ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
30 18 21 24 29 mp3an 
 |-  1 = ( 0g ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
31 30 ghmker 
 |-  ( ( pmSgn ` D ) e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> ( `' ( pmSgn ` D ) " { 1 } ) e. ( NrmSGrp ` S ) )
32 14 31 syl 
 |-  ( D e. Fin -> ( `' ( pmSgn ` D ) " { 1 } ) e. ( NrmSGrp ` S ) )
33 11 32 eqeltrd 
 |-  ( D e. Fin -> ( pmEven ` D ) e. ( NrmSGrp ` S ) )