This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zrhpsgninv

Description: The embedded sign of a permutation equals the embedded sign of the inverse of the permutation. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses zrhpsgninv.p 
|- P = ( Base ` ( SymGrp ` N ) )
zrhpsgninv.y 
|- Y = ( ZRHom ` R )
zrhpsgninv.s 
|- S = ( pmSgn ` N )
Assertion zrhpsgninv 
|- ( ( R e. Ring /\ N e. Fin /\ F e. P ) -> ( ( Y o. S ) ` `' F ) = ( ( Y o. S ) ` F ) )

Proof

Step Hyp Ref Expression
1 zrhpsgninv.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 zrhpsgninv.y 
 |-  Y = ( ZRHom ` R )
3 zrhpsgninv.s 
 |-  S = ( pmSgn ` N )
4 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
5 4 3 1 psgninv 
 |-  ( ( N e. Fin /\ F e. P ) -> ( S ` `' F ) = ( S ` F ) )
6 5 3adant1 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. P ) -> ( S ` `' F ) = ( S ` F ) )
7 6 fveq2d 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. P ) -> ( Y ` ( S ` `' F ) ) = ( Y ` ( S ` F ) ) )
8 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
9 4 3 8 psgnghm2 
 |-  ( N e. Fin -> S e. ( ( SymGrp ` N ) GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
10 eqid 
 |-  ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) = ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
11 1 10 ghmf 
 |-  ( S e. ( ( SymGrp ` N ) GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> S : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
12 9 11 syl 
 |-  ( N e. Fin -> S : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
13 12 3ad2ant2 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. P ) -> S : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
14 eqid 
 |-  ( invg ` ( SymGrp ` N ) ) = ( invg ` ( SymGrp ` N ) )
15 4 1 14 symginv 
 |-  ( F e. P -> ( ( invg ` ( SymGrp ` N ) ) ` F ) = `' F )
16 15 3ad2ant3 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. P ) -> ( ( invg ` ( SymGrp ` N ) ) ` F ) = `' F )
17 4 symggrp 
 |-  ( N e. Fin -> ( SymGrp ` N ) e. Grp )
18 17 3ad2ant2 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. P ) -> ( SymGrp ` N ) e. Grp )
19 simp3 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. P ) -> F e. P )
20 1 14 grpinvcl 
 |-  ( ( ( SymGrp ` N ) e. Grp /\ F e. P ) -> ( ( invg ` ( SymGrp ` N ) ) ` F ) e. P )
21 18 19 20 syl2anc 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. P ) -> ( ( invg ` ( SymGrp ` N ) ) ` F ) e. P )
22 16 21 eqeltrrd 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. P ) -> `' F e. P )
23 fvco3 
 |-  ( ( S : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) /\ `' F e. P ) -> ( ( Y o. S ) ` `' F ) = ( Y ` ( S ` `' F ) ) )
24 13 22 23 syl2anc 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. P ) -> ( ( Y o. S ) ` `' F ) = ( Y ` ( S ` `' F ) ) )
25 fvco3 
 |-  ( ( S : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) /\ F e. P ) -> ( ( Y o. S ) ` F ) = ( Y ` ( S ` F ) ) )
26 13 19 25 syl2anc 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. P ) -> ( ( Y o. S ) ` F ) = ( Y ` ( S ` F ) ) )
27 7 24 26 3eqtr4d 
 |-  ( ( R e. Ring /\ N e. Fin /\ F e. P ) -> ( ( Y o. S ) ` `' F ) = ( ( Y o. S ) ` F ) )