Metamath Proof Explorer

Theorem zrhpsgnodpm

Description: The sign of an odd permutation embedded into a ring is the additive inverse of the multiplicative neutral element of the ring. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses zrhpsgnevpm.y 
|- Y = ( ZRHom ` R )
zrhpsgnevpm.s 
|- S = ( pmSgn ` N )
zrhpsgnevpm.o 
|- .1. = ( 1r ` R )
zrhpsgnodpm.p 
|- P = ( Base ` ( SymGrp ` N ) )
zrhpsgnodpm.i 
|- I = ( invg ` R )
Assertion zrhpsgnodpm 
|- ( ( R e. Ring /\ N e. Fin /\ F e. ( P \ ( pmEven ` N ) ) ) -> ( ( Y o. S ) ` F ) = ( I ` .1. ) )

Proof

Step Hyp Ref Expression
1 zrhpsgnevpm.y 
 |-  Y = ( ZRHom ` R )
2 zrhpsgnevpm.s 
 |-  S = ( pmSgn ` N )
3 zrhpsgnevpm.o 
 |-  .1. = ( 1r ` R )
4 zrhpsgnodpm.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
5 zrhpsgnodpm.i 
 |-  I = ( invg ` R )
6 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
7 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
8 6 2 7 psgnghm2 
 |-  ( N e. Fin -> S e. ( ( SymGrp ` N ) GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
9 eqid 
 |-  ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) = ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
10 4 9 ghmf 
 |-  ( S e. ( ( SymGrp ` N ) GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> S : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
11 8 10 syl 
 |-  ( N e. Fin -> S : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
12 11 3ad2ant2 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. ( P \ ( pmEven ` N ) ) ) -> S : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
13 eldifi 
 |-  ( F e. ( P \ ( pmEven ` N ) ) -> F e. P )
14 13 3ad2ant3 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. ( P \ ( pmEven ` N ) ) ) -> F e. P )
15 fvco3 
 |-  ( ( S : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) /\ F e. P ) -> ( ( Y o. S ) ` F ) = ( Y ` ( S ` F ) ) )
16 12 14 15 syl2anc 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. ( P \ ( pmEven ` N ) ) ) -> ( ( Y o. S ) ` F ) = ( Y ` ( S ` F ) ) )
17 6 4 2 psgnodpm 
 |-  ( ( N e. Fin /\ F e. ( P \ ( pmEven ` N ) ) ) -> ( S ` F ) = -u 1 )
18 17 3adant1 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. ( P \ ( pmEven ` N ) ) ) -> ( S ` F ) = -u 1 )
19 18 fveq2d 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. ( P \ ( pmEven ` N ) ) ) -> ( Y ` ( S ` F ) ) = ( Y ` -u 1 ) )
20 1 zrhrhm 
 |-  ( R e. Ring -> Y e. ( ZZring RingHom R ) )
21 rhmghm 
 |-  ( Y e. ( ZZring RingHom R ) -> Y e. ( ZZring GrpHom R ) )
22 20 21 syl 
 |-  ( R e. Ring -> Y e. ( ZZring GrpHom R ) )
23 1z 
 |-  1 e. ZZ
24 23 a1i 
 |-  ( R e. Ring -> 1 e. ZZ )
25 zringbas 
 |-  ZZ = ( Base ` ZZring )
26 eqid 
 |-  ( invg ` ZZring ) = ( invg ` ZZring )
27 25 26 5 ghminv 
 |-  ( ( Y e. ( ZZring GrpHom R ) /\ 1 e. ZZ ) -> ( Y ` ( ( invg ` ZZring ) ` 1 ) ) = ( I ` ( Y ` 1 ) ) )
28 22 24 27 syl2anc 
 |-  ( R e. Ring -> ( Y ` ( ( invg ` ZZring ) ` 1 ) ) = ( I ` ( Y ` 1 ) ) )
29 zringinvg 
 |-  ( 1 e. ZZ -> -u 1 = ( ( invg ` ZZring ) ` 1 ) )
30 23 29 ax-mp 
 |-  -u 1 = ( ( invg ` ZZring ) ` 1 )
31 30 eqcomi 
 |-  ( ( invg ` ZZring ) ` 1 ) = -u 1
32 31 fveq2i 
 |-  ( Y ` ( ( invg ` ZZring ) ` 1 ) ) = ( Y ` -u 1 )
33 32 a1i 
 |-  ( R e. Ring -> ( Y ` ( ( invg ` ZZring ) ` 1 ) ) = ( Y ` -u 1 ) )
34 1 3 zrh1 
 |-  ( R e. Ring -> ( Y ` 1 ) = .1. )
35 34 fveq2d 
 |-  ( R e. Ring -> ( I ` ( Y ` 1 ) ) = ( I ` .1. ) )
36 28 33 35 3eqtr3d 
 |-  ( R e. Ring -> ( Y ` -u 1 ) = ( I ` .1. ) )
37 36 3ad2ant1 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. ( P \ ( pmEven ` N ) ) ) -> ( Y ` -u 1 ) = ( I ` .1. ) )
38 16 19 37 3eqtrd 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. ( P \ ( pmEven ` N ) ) ) -> ( ( Y o. S ) ` F ) = ( I ` .1. ) )