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

Metamath Proof Explorer

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