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 ) )