Theorem cofipsgn

Description: Composition of any class Y and the sign function for a finite permutation. (Contributed by AV, 27-Dec-2018) (Revised by AV, 3-Jul-2022)

	Ref	Expression
Hypotheses	cofipsgn.p	|- P = ( Base ` ( SymGrp ` N ) )
	cofipsgn.s	|- S = ( pmSgn ` N )
Assertion	cofipsgn	|- ( ( N e. Fin /\ Q e. P ) -> ( ( Y o. S ) ` Q ) = ( Y ` ( S ` Q ) ) )

Proof

Step	Hyp	Ref	Expression
1		cofipsgn.p	|- P = ( Base ` ( SymGrp ` N ) )
2		cofipsgn.s	|- S = ( pmSgn ` N )
3		eqid	|- ( SymGrp ` N ) = ( SymGrp ` N )
4		eqid	|- { p e. P | dom ( p \ _I ) e. Fin } = { p e. P | dom ( p \ _I ) e. Fin }
5	3 1 4 2	psgnfn	|- S Fn { p e. P | dom ( p \ _I ) e. Fin }
6		difeq1	|- ( p = Q -> ( p \ _I ) = ( Q \ _I ) )
7	6	dmeqd	|- ( p = Q -> dom ( p \ _I ) = dom ( Q \ _I ) )
8	7	eleq1d	|- ( p = Q -> ( dom ( p \ _I ) e. Fin <-> dom ( Q \ _I ) e. Fin ) )
9		simpr	|- ( ( N e. Fin /\ Q e. P ) -> Q e. P )
10	3 1	sygbasnfpfi	|- ( ( N e. Fin /\ Q e. P ) -> dom ( Q \ _I ) e. Fin )
11	8 9 10	elrabd	|- ( ( N e. Fin /\ Q e. P ) -> Q e. { p e. P | dom ( p \ _I ) e. Fin } )
12		fvco2	|- ( ( S Fn { p e. P | dom ( p \ _I ) e. Fin } /\ Q e. { p e. P | dom ( p \ _I ) e. Fin } ) -> ( ( Y o. S ) ` Q ) = ( Y ` ( S ` Q ) ) )
13	5 11 12	sylancr	|- ( ( N e. Fin /\ Q e. P ) -> ( ( Y o. S ) ` Q ) = ( Y ` ( S ` Q ) ) )