Theorem copsgndif

Description: Embedding of permutation signs restricted to a set without a single element into a ring. (Contributed by AV, 31-Jan-2019) (Revised by AV, 5-Jul-2022)

	Ref	Expression
Hypotheses	copsgndif.p	|- P = ( Base ` ( SymGrp ` N ) )
	copsgndif.s	|- S = ( pmSgn ` N )
	copsgndif.z	|- Z = ( pmSgn ` ( N \ { K } ) )
Assertion	copsgndif	|- ( ( N e. Fin /\ K e. N ) -> ( Q e. { q e. P | ( q ` K ) = K } -> ( ( Y o. Z ) ` ( Q |` ( N \ { K } ) ) ) = ( ( Y o. S ) ` Q ) ) )

Proof

Step	Hyp	Ref	Expression
1		copsgndif.p	|- P = ( Base ` ( SymGrp ` N ) )
2		copsgndif.s	|- S = ( pmSgn ` N )
3		copsgndif.z	|- Z = ( pmSgn ` ( N \ { K } ) )
4	1 2 3	psgndif	|- ( ( N e. Fin /\ K e. N ) -> ( Q e. { q e. P | ( q ` K ) = K } -> ( Z ` ( Q |` ( N \ { K } ) ) ) = ( S ` Q ) ) )
5	4	imp	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( Z ` ( Q |` ( N \ { K } ) ) ) = ( S ` Q ) )
6	5	fveq2d	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( Y ` ( Z ` ( Q |` ( N \ { K } ) ) ) ) = ( Y ` ( S ` Q ) ) )
7		diffi	|- ( N e. Fin -> ( N \ { K } ) e. Fin )
8	7	ad2antrr	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( N \ { K } ) e. Fin )
9		eqid	|- { q e. P | ( q ` K ) = K } = { q e. P | ( q ` K ) = K }
10		eqid	|- ( Base ` ( SymGrp ` ( N \ { K } ) ) ) = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
11		eqid	|- ( N \ { K } ) = ( N \ { K } )
12	1 9 10 11	symgfixelsi	|- ( ( K e. N /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( Q |` ( N \ { K } ) ) e. ( Base ` ( SymGrp ` ( N \ { K } ) ) ) )
13	12	adantll	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( Q |` ( N \ { K } ) ) e. ( Base ` ( SymGrp ` ( N \ { K } ) ) ) )
14	10 3	cofipsgn	|- ( ( ( N \ { K } ) e. Fin /\ ( Q |` ( N \ { K } ) ) e. ( Base ` ( SymGrp ` ( N \ { K } ) ) ) ) -> ( ( Y o. Z ) ` ( Q |` ( N \ { K } ) ) ) = ( Y ` ( Z ` ( Q |` ( N \ { K } ) ) ) ) )
15	8 13 14	syl2anc	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( ( Y o. Z ) ` ( Q |` ( N \ { K } ) ) ) = ( Y ` ( Z ` ( Q |` ( N \ { K } ) ) ) ) )
16		elrabi	|- ( Q e. { q e. P | ( q ` K ) = K } -> Q e. P )
17	1 2	cofipsgn	|- ( ( N e. Fin /\ Q e. P ) -> ( ( Y o. S ) ` Q ) = ( Y ` ( S ` Q ) ) )
18	16 17	sylan2	|- ( ( N e. Fin /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( ( Y o. S ) ` Q ) = ( Y ` ( S ` Q ) ) )
19	18	adantlr	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( ( Y o. S ) ` Q ) = ( Y ` ( S ` Q ) ) )
20	6 15 19	3eqtr4d	|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( ( Y o. Z ) ` ( Q |` ( N \ { K } ) ) ) = ( ( Y o. S ) ` Q ) )
21	20	ex	|- ( ( N e. Fin /\ K e. N ) -> ( Q e. { q e. P | ( q ` K ) = K } -> ( ( Y o. Z ) ` ( Q |` ( N \ { K } ) ) ) = ( ( Y o. S ) ` Q ) ) )