Metamath Proof Explorer

Theorem psgnid

Description: Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020)

Ref Expression
Hypothesis psgnid.s 
|- S = ( pmSgn ` D )
Assertion psgnid 
|- ( D e. Fin -> ( S ` ( _I |` D ) ) = 1 )

Proof

Step Hyp Ref Expression
1 psgnid.s 
 |-  S = ( pmSgn ` D )
2 eqid 
 |-  ( SymGrp ` D ) = ( SymGrp ` D )
3 2 symgid 
 |-  ( D e. Fin -> ( _I |` D ) = ( 0g ` ( SymGrp ` D ) ) )
4 3 fveq2d 
 |-  ( D e. Fin -> ( S ` ( _I |` D ) ) = ( S ` ( 0g ` ( SymGrp ` D ) ) ) )
5 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
6 2 1 5 psgnghm2 
 |-  ( D e. Fin -> S e. ( ( SymGrp ` D ) GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
7 eqid 
 |-  ( 0g ` ( SymGrp ` D ) ) = ( 0g ` ( SymGrp ` D ) )
8 cnring 
 |-  CCfld e. Ring
9 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
10 9 ringmgp 
 |-  ( CCfld e. Ring -> ( mulGrp ` CCfld ) e. Mnd )
11 8 10 ax-mp 
 |-  ( mulGrp ` CCfld ) e. Mnd
12 1ex 
 |-  1 e. _V
13 12 prid1 
 |-  1 e. { 1 , -u 1 }
14 ax-1cn 
 |-  1 e. CC
15 neg1cn 
 |-  -u 1 e. CC
16 prssi 
 |-  ( ( 1 e. CC /\ -u 1 e. CC ) -> { 1 , -u 1 } C_ CC )
17 14 15 16 mp2an 
 |-  { 1 , -u 1 } C_ CC
18 cnfldbas 
 |-  CC = ( Base ` CCfld )
19 9 18 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
20 cnfld1 
 |-  1 = ( 1r ` CCfld )
21 9 20 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
22 5 19 21 ress0g 
 |-  ( ( ( mulGrp ` CCfld ) e. Mnd /\ 1 e. { 1 , -u 1 } /\ { 1 , -u 1 } C_ CC ) -> 1 = ( 0g ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
23 11 13 17 22 mp3an 
 |-  1 = ( 0g ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
24 7 23 ghmid 
 |-  ( S e. ( ( SymGrp ` D ) GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> ( S ` ( 0g ` ( SymGrp ` D ) ) ) = 1 )
25 6 24 syl 
 |-  ( D e. Fin -> ( S ` ( 0g ` ( SymGrp ` D ) ) ) = 1 )
26 4 25 eqtrd 
 |-  ( D e. Fin -> ( S ` ( _I |` D ) ) = 1 )