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

Metamath Proof Explorer

Theorem psgndif

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

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

Proof

Step Hyp Ref Expression
1 psgndif.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 psgndif.s 
 |-  S = ( pmSgn ` N )
3 psgndif.z 
 |-  Z = ( pmSgn ` ( N \ { K } ) )
4 eqid 
 |-  ran ( pmTrsp ` ( N \ { K } ) ) = ran ( pmTrsp ` ( N \ { K } ) )
5 eqid 
 |-  ( SymGrp ` ( N \ { K } ) ) = ( SymGrp ` ( N \ { K } ) )
6 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
7 eqid 
 |-  ran ( pmTrsp ` N ) = ran ( pmTrsp ` N )
8 1 4 5 6 7 psgnfix2 
 |-  ( ( N e. Fin /\ K e. N ) -> ( Q e. { q e. P | ( q ` K ) = K } -> E. r e. Word ran ( pmTrsp ` N ) Q = ( ( SymGrp ` N ) gsum r ) ) )
9 8 imp 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> E. r e. Word ran ( pmTrsp ` N ) Q = ( ( SymGrp ` N ) gsum r ) )
10 9 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) -> E. r e. Word ran ( pmTrsp ` N ) Q = ( ( SymGrp ` N ) gsum r ) )
11 1 4 5 6 7 psgndiflemA 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( ( w e. Word ran ( pmTrsp ` ( N \ { K } ) ) /\ ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ r e. Word ran ( pmTrsp ` N ) ) -> ( Q = ( ( SymGrp ` N ) gsum r ) -> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` r ) ) ) ) )
12 11 imp 
 |-  ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( w e. Word ran ( pmTrsp ` ( N \ { K } ) ) /\ ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ r e. Word ran ( pmTrsp ` N ) ) ) -> ( Q = ( ( SymGrp ` N ) gsum r ) -> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` r ) ) ) )
13 12 3anassrs 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) ) /\ r e. Word ran ( pmTrsp ` N ) ) -> ( Q = ( ( SymGrp ` N ) gsum r ) -> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` r ) ) ) )
14 13 adantlrr 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) /\ r e. Word ran ( pmTrsp ` N ) ) -> ( Q = ( ( SymGrp ` N ) gsum r ) -> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` r ) ) ) )
15 eqeq1 
 |-  ( s = ( -u 1 ^ ( # ` w ) ) -> ( s = ( -u 1 ^ ( # ` r ) ) <-> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` r ) ) ) )
16 15 ad2antll 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) -> ( s = ( -u 1 ^ ( # ` r ) ) <-> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` r ) ) ) )
17 16 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) /\ r e. Word ran ( pmTrsp ` N ) ) -> ( s = ( -u 1 ^ ( # ` r ) ) <-> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` r ) ) ) )
18 14 17 sylibrd 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) /\ r e. Word ran ( pmTrsp ` N ) ) -> ( Q = ( ( SymGrp ` N ) gsum r ) -> s = ( -u 1 ^ ( # ` r ) ) ) )
19 18 ralrimiva 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) -> A. r e. Word ran ( pmTrsp ` N ) ( Q = ( ( SymGrp ` N ) gsum r ) -> s = ( -u 1 ^ ( # ` r ) ) ) )
20 10 19 r19.29imd 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) -> E. r e. Word ran ( pmTrsp ` N ) ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) )
21 20 rexlimdva2 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( E. w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) -> E. r e. Word ran ( pmTrsp ` N ) ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) ) )
22 1 4 5 psgnfix1 
 |-  ( ( N e. Fin /\ K e. N ) -> ( Q e. { q e. P | ( q ` K ) = K } -> E. w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) ) )
23 22 imp 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> E. w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) )
24 23 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) ) -> E. w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) )
25 simp-4l 
 |-  ( ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ Q = ( ( SymGrp ` N ) gsum r ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) ) -> ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) )
26 simpr 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ Q = ( ( SymGrp ` N ) gsum r ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) -> w e. Word ran ( pmTrsp ` ( N \ { K } ) ) )
27 26 adantr 
 |-  ( ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ Q = ( ( SymGrp ` N ) gsum r ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) ) -> w e. Word ran ( pmTrsp ` ( N \ { K } ) ) )
28 simpr 
 |-  ( ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ Q = ( ( SymGrp ` N ) gsum r ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) ) -> ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) )
29 simp-4r 
 |-  ( ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ Q = ( ( SymGrp ` N ) gsum r ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) ) -> r e. Word ran ( pmTrsp ` N ) )
30 27 28 29 3jca 
 |-  ( ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ Q = ( ( SymGrp ` N ) gsum r ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) ) -> ( w e. Word ran ( pmTrsp ` ( N \ { K } ) ) /\ ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ r e. Word ran ( pmTrsp ` N ) ) )
31 simpr 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ Q = ( ( SymGrp ` N ) gsum r ) ) -> Q = ( ( SymGrp ` N ) gsum r ) )
32 31 ad2antrr 
 |-  ( ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ Q = ( ( SymGrp ` N ) gsum r ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) ) -> Q = ( ( SymGrp ` N ) gsum r ) )
33 25 30 32 11 syl3c 
 |-  ( ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ Q = ( ( SymGrp ` N ) gsum r ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) ) -> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` r ) ) )
34 33 eqcomd 
 |-  ( ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ Q = ( ( SymGrp ` N ) gsum r ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) /\ ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) ) -> ( -u 1 ^ ( # ` r ) ) = ( -u 1 ^ ( # ` w ) ) )
35 34 ex 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ Q = ( ( SymGrp ` N ) gsum r ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) -> ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) -> ( -u 1 ^ ( # ` r ) ) = ( -u 1 ^ ( # ` w ) ) ) )
36 35 adantlrr 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) -> ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) -> ( -u 1 ^ ( # ` r ) ) = ( -u 1 ^ ( # ` w ) ) ) )
37 eqeq1 
 |-  ( s = ( -u 1 ^ ( # ` r ) ) -> ( s = ( -u 1 ^ ( # ` w ) ) <-> ( -u 1 ^ ( # ` r ) ) = ( -u 1 ^ ( # ` w ) ) ) )
38 37 ad2antll 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) ) -> ( s = ( -u 1 ^ ( # ` w ) ) <-> ( -u 1 ^ ( # ` r ) ) = ( -u 1 ^ ( # ` w ) ) ) )
39 38 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) -> ( s = ( -u 1 ^ ( # ` w ) ) <-> ( -u 1 ^ ( # ` r ) ) = ( -u 1 ^ ( # ` w ) ) ) )
40 36 39 sylibrd 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) ) /\ w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ) -> ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) -> s = ( -u 1 ^ ( # ` w ) ) ) )
41 40 ralrimiva 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) ) -> A. w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) -> s = ( -u 1 ^ ( # ` w ) ) ) )
42 24 41 r19.29imd 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ r e. Word ran ( pmTrsp ` N ) ) /\ ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) ) -> E. w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
43 42 rexlimdva2 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( E. r e. Word ran ( pmTrsp ` N ) ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) -> E. w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
44 21 43 impbid 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( E. w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> E. r e. Word ran ( pmTrsp ` N ) ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) ) )
45 44 iotabidv 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( iota s E. w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) = ( iota s E. r e. Word ran ( pmTrsp ` N ) ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) ) )
46 diffi 
 |-  ( N e. Fin -> ( N \ { K } ) e. Fin )
47 46 ad2antrr 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( N \ { K } ) e. Fin )
48 eqid 
 |-  { q e. P | ( q ` K ) = K } = { q e. P | ( q ` K ) = K }
49 eqid 
 |-  ( Base ` ( SymGrp ` ( N \ { K } ) ) ) = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
50 eqid 
 |-  ( N \ { K } ) = ( N \ { K } )
51 1 48 49 50 symgfixelsi 
 |-  ( ( K e. N /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( Q |` ( N \ { K } ) ) e. ( Base ` ( SymGrp ` ( N \ { K } ) ) ) )
52 51 adantll 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( Q |` ( N \ { K } ) ) e. ( Base ` ( SymGrp ` ( N \ { K } ) ) ) )
53 5 49 4 3 psgnvalfi 
 |-  ( ( ( N \ { K } ) e. Fin /\ ( Q |` ( N \ { K } ) ) e. ( Base ` ( SymGrp ` ( N \ { K } ) ) ) ) -> ( Z ` ( Q |` ( N \ { K } ) ) ) = ( iota s E. w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
54 47 52 53 syl2anc 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( Z ` ( Q |` ( N \ { K } ) ) ) = ( iota s E. w e. Word ran ( pmTrsp ` ( N \ { K } ) ) ( ( Q |` ( N \ { K } ) ) = ( ( SymGrp ` ( N \ { K } ) ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
55 simpl 
 |-  ( ( N e. Fin /\ K e. N ) -> N e. Fin )
56 elrabi 
 |-  ( Q e. { q e. P | ( q ` K ) = K } -> Q e. P )
57 6 1 7 2 psgnvalfi 
 |-  ( ( N e. Fin /\ Q e. P ) -> ( S ` Q ) = ( iota s E. r e. Word ran ( pmTrsp ` N ) ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) ) )
58 55 56 57 syl2an 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( S ` Q ) = ( iota s E. r e. Word ran ( pmTrsp ` N ) ( Q = ( ( SymGrp ` N ) gsum r ) /\ s = ( -u 1 ^ ( # ` r ) ) ) ) )
59 45 54 58 3eqtr4d 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( Z ` ( Q |` ( N \ { K } ) ) ) = ( S ` Q ) )
60 59 ex 
 |-  ( ( N e. Fin /\ K e. N ) -> ( Q e. { q e. P | ( q ` K ) = K } -> ( Z ` ( Q |` ( N \ { K } ) ) ) = ( S ` Q ) ) )