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

Metamath Proof Explorer

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