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

Metamath Proof Explorer

Theorem psgndiflemB

Description: Lemma 1 for psgndif . (Contributed by AV, 27-Jan-2019)

Ref Expression
Hypotheses psgnfix.p 
|- P = ( Base ` ( SymGrp ` N ) )
psgnfix.t 
|- T = ran ( pmTrsp ` ( N \ { K } ) )
psgnfix.s 
|- S = ( SymGrp ` ( N \ { K } ) )
psgnfix.z 
|- Z = ( SymGrp ` N )
psgnfix.r 
|- R = ran ( pmTrsp ` N )
Assertion psgndiflemB 
|- ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) -> ( ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) -> Q = ( Z gsum U ) ) ) )

Proof

Step Hyp Ref Expression
1 psgnfix.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 psgnfix.t 
 |-  T = ran ( pmTrsp ` ( N \ { K } ) )
3 psgnfix.s 
 |-  S = ( SymGrp ` ( N \ { K } ) )
4 psgnfix.z 
 |-  Z = ( SymGrp ` N )
5 psgnfix.r 
 |-  R = ran ( pmTrsp ` N )
6 elrabi 
 |-  ( Q e. { q e. P | ( q ` K ) = K } -> Q e. P )
7 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
8 7 1 symgbasf 
 |-  ( Q e. P -> Q : N --> N )
9 ffn 
 |-  ( Q : N --> N -> Q Fn N )
10 6 8 9 3syl 
 |-  ( Q e. { q e. P | ( q ` K ) = K } -> Q Fn N )
11 10 ad3antlr 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> Q Fn N )
12 simpl 
 |-  ( ( N e. Fin /\ K e. N ) -> N e. Fin )
13 12 adantr 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> N e. Fin )
14 13 adantr 
 |-  ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) -> N e. Fin )
15 simp1 
 |-  ( ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) -> U e. Word R )
16 4 eqcomi 
 |-  ( SymGrp ` N ) = Z
17 16 fveq2i 
 |-  ( Base ` ( SymGrp ` N ) ) = ( Base ` Z )
18 1 17 eqtri 
 |-  P = ( Base ` Z )
19 4 18 5 gsmtrcl 
 |-  ( ( N e. Fin /\ U e. Word R ) -> ( Z gsum U ) e. P )
20 14 15 19 syl2an 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> ( Z gsum U ) e. P )
21 7 1 symgbasf 
 |-  ( ( Z gsum U ) e. P -> ( Z gsum U ) : N --> N )
22 ffn 
 |-  ( ( Z gsum U ) : N --> N -> ( Z gsum U ) Fn N )
23 20 21 22 3syl 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> ( Z gsum U ) Fn N )
24 12 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> N e. Fin )
25 simpr 
 |-  ( ( N e. Fin /\ K e. N ) -> K e. N )
26 25 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> K e. N )
27 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
28 5 4 27 symgtrf 
 |-  R C_ ( Base ` Z )
29 sswrd 
 |-  ( R C_ ( Base ` Z ) -> Word R C_ Word ( Base ` Z ) )
30 29 sseld 
 |-  ( R C_ ( Base ` Z ) -> ( U e. Word R -> U e. Word ( Base ` Z ) ) )
31 28 30 ax-mp 
 |-  ( U e. Word R -> U e. Word ( Base ` Z ) )
32 31 3ad2ant1 
 |-  ( ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) -> U e. Word ( Base ` Z ) )
33 32 adantl 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> U e. Word ( Base ` Z ) )
34 24 26 33 3jca 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> ( N e. Fin /\ K e. N /\ U e. Word ( Base ` Z ) ) )
35 simpl 
 |-  ( ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) -> ( ( U ` i ) ` K ) = K )
36 35 ralimi 
 |-  ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( ( U ` i ) ` K ) = K )
37 36 3ad2ant3 
 |-  ( ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( ( U ` i ) ` K ) = K )
38 37 adantl 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( ( U ` i ) ` K ) = K )
39 oveq2 
 |-  ( ( # ` U ) = ( # ` W ) -> ( 0 ..^ ( # ` U ) ) = ( 0 ..^ ( # ` W ) ) )
40 39 eqcoms 
 |-  ( ( # ` W ) = ( # ` U ) -> ( 0 ..^ ( # ` U ) ) = ( 0 ..^ ( # ` W ) ) )
41 40 raleqdv 
 |-  ( ( # ` W ) = ( # ` U ) -> ( A. i e. ( 0 ..^ ( # ` U ) ) ( ( U ` i ) ` K ) = K <-> A. i e. ( 0 ..^ ( # ` W ) ) ( ( U ` i ) ` K ) = K ) )
42 41 3ad2ant2 
 |-  ( ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) -> ( A. i e. ( 0 ..^ ( # ` U ) ) ( ( U ` i ) ` K ) = K <-> A. i e. ( 0 ..^ ( # ` W ) ) ( ( U ` i ) ` K ) = K ) )
43 42 adantl 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> ( A. i e. ( 0 ..^ ( # ` U ) ) ( ( U ` i ) ` K ) = K <-> A. i e. ( 0 ..^ ( # ` W ) ) ( ( U ` i ) ` K ) = K ) )
44 38 43 mpbird 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> A. i e. ( 0 ..^ ( # ` U ) ) ( ( U ` i ) ` K ) = K )
45 4 27 gsmsymgrfix 
 |-  ( ( N e. Fin /\ K e. N /\ U e. Word ( Base ` Z ) ) -> ( A. i e. ( 0 ..^ ( # ` U ) ) ( ( U ` i ) ` K ) = K -> ( ( Z gsum U ) ` K ) = K ) )
46 34 44 45 sylc 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> ( ( Z gsum U ) ` K ) = K )
47 46 eqcomd 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> K = ( ( Z gsum U ) ` K ) )
48 47 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k = K ) -> K = ( ( Z gsum U ) ` K ) )
49 fveq2 
 |-  ( k = K -> ( Q ` k ) = ( Q ` K ) )
50 fveq1 
 |-  ( q = Q -> ( q ` K ) = ( Q ` K ) )
51 50 eqeq1d 
 |-  ( q = Q -> ( ( q ` K ) = K <-> ( Q ` K ) = K ) )
52 51 elrab 
 |-  ( Q e. { q e. P | ( q ` K ) = K } <-> ( Q e. P /\ ( Q ` K ) = K ) )
53 52 simprbi 
 |-  ( Q e. { q e. P | ( q ` K ) = K } -> ( Q ` K ) = K )
54 53 ad3antlr 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> ( Q ` K ) = K )
55 49 54 sylan9eqr 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k = K ) -> ( Q ` k ) = K )
56 fveq2 
 |-  ( k = K -> ( ( Z gsum U ) ` k ) = ( ( Z gsum U ) ` K ) )
57 56 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k = K ) -> ( ( Z gsum U ) ` k ) = ( ( Z gsum U ) ` K ) )
58 48 55 57 3eqtr4d 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k = K ) -> ( Q ` k ) = ( ( Z gsum U ) ` k ) )
59 58 ex 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> ( k = K -> ( Q ` k ) = ( ( Z gsum U ) ` k ) ) )
60 59 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) -> ( k = K -> ( Q ` k ) = ( ( Z gsum U ) ` k ) ) )
61 60 com12 
 |-  ( k = K -> ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) -> ( Q ` k ) = ( ( Z gsum U ) ` k ) ) )
62 fveq1 
 |-  ( ( Q |` ( N \ { K } ) ) = ( S gsum W ) -> ( ( Q |` ( N \ { K } ) ) ` k ) = ( ( S gsum W ) ` k ) )
63 62 adantl 
 |-  ( ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) -> ( ( Q |` ( N \ { K } ) ) ` k ) = ( ( S gsum W ) ` k ) )
64 63 ad3antlr 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) -> ( ( Q |` ( N \ { K } ) ) ` k ) = ( ( S gsum W ) ` k ) )
65 64 adantl 
 |-  ( ( -. k = K /\ ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) ) -> ( ( Q |` ( N \ { K } ) ) ` k ) = ( ( S gsum W ) ` k ) )
66 simpr 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ k e. N ) -> k e. N )
67 neqne 
 |-  ( -. k = K -> k =/= K )
68 66 67 anim12i 
 |-  ( ( ( ( N e. Fin /\ K e. N ) /\ k e. N ) /\ -. k = K ) -> ( k e. N /\ k =/= K ) )
69 eldifsn 
 |-  ( k e. ( N \ { K } ) <-> ( k e. N /\ k =/= K ) )
70 68 69 sylibr 
 |-  ( ( ( ( N e. Fin /\ K e. N ) /\ k e. N ) /\ -. k = K ) -> k e. ( N \ { K } ) )
71 70 fvresd 
 |-  ( ( ( ( N e. Fin /\ K e. N ) /\ k e. N ) /\ -. k = K ) -> ( ( Q |` ( N \ { K } ) ) ` k ) = ( Q ` k ) )
72 71 exp31 
 |-  ( ( N e. Fin /\ K e. N ) -> ( k e. N -> ( -. k = K -> ( ( Q |` ( N \ { K } ) ) ` k ) = ( Q ` k ) ) ) )
73 72 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> ( k e. N -> ( -. k = K -> ( ( Q |` ( N \ { K } ) ) ` k ) = ( Q ` k ) ) ) )
74 73 imp 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) -> ( -. k = K -> ( ( Q |` ( N \ { K } ) ) ` k ) = ( Q ` k ) ) )
75 74 impcom 
 |-  ( ( -. k = K /\ ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) ) -> ( ( Q |` ( N \ { K } ) ) ` k ) = ( Q ` k ) )
76 fveq2 
 |-  ( n = k -> ( ( S gsum W ) ` n ) = ( ( S gsum W ) ` k ) )
77 fveq2 
 |-  ( n = k -> ( ( Z gsum U ) ` n ) = ( ( Z gsum U ) ` k ) )
78 76 77 eqeq12d 
 |-  ( n = k -> ( ( ( S gsum W ) ` n ) = ( ( Z gsum U ) ` n ) <-> ( ( S gsum W ) ` k ) = ( ( Z gsum U ) ` k ) ) )
79 diffi 
 |-  ( N e. Fin -> ( N \ { K } ) e. Fin )
80 79 ancri 
 |-  ( N e. Fin -> ( ( N \ { K } ) e. Fin /\ N e. Fin ) )
81 80 adantr 
 |-  ( ( N e. Fin /\ K e. N ) -> ( ( N \ { K } ) e. Fin /\ N e. Fin ) )
82 81 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> ( ( N \ { K } ) e. Fin /\ N e. Fin ) )
83 eqid 
 |-  ( Base ` S ) = ( Base ` S )
84 2 3 83 symgtrf 
 |-  T C_ ( Base ` S )
85 sswrd 
 |-  ( T C_ ( Base ` S ) -> Word T C_ Word ( Base ` S ) )
86 85 sseld 
 |-  ( T C_ ( Base ` S ) -> ( W e. Word T -> W e. Word ( Base ` S ) ) )
87 84 86 ax-mp 
 |-  ( W e. Word T -> W e. Word ( Base ` S ) )
88 87 ad2antrl 
 |-  ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) -> W e. Word ( Base ` S ) )
89 88 adantr 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> W e. Word ( Base ` S ) )
90 simpr2 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> ( # ` W ) = ( # ` U ) )
91 89 33 90 3jca 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> ( W e. Word ( Base ` S ) /\ U e. Word ( Base ` Z ) /\ ( # ` W ) = ( # ` U ) ) )
92 82 91 jca 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> ( ( ( N \ { K } ) e. Fin /\ N e. Fin ) /\ ( W e. Word ( Base ` S ) /\ U e. Word ( Base ` Z ) /\ ( # ` W ) = ( # ` U ) ) ) )
93 92 ad2antrl 
 |-  ( ( -. k = K /\ ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) ) -> ( ( ( N \ { K } ) e. Fin /\ N e. Fin ) /\ ( W e. Word ( Base ` S ) /\ U e. Word ( Base ` Z ) /\ ( # ` W ) = ( # ` U ) ) ) )
94 simpr 
 |-  ( ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) -> A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) )
95 94 ralimi 
 |-  ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) )
96 95 3ad2ant3 
 |-  ( ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) )
97 96 adantl 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) )
98 97 ad2antrl 
 |-  ( ( -. k = K /\ ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) )
99 incom 
 |-  ( ( N \ { K } ) i^i N ) = ( N i^i ( N \ { K } ) )
100 indif 
 |-  ( N i^i ( N \ { K } ) ) = ( N \ { K } )
101 99 100 eqtri 
 |-  ( ( N \ { K } ) i^i N ) = ( N \ { K } )
102 101 eqcomi 
 |-  ( N \ { K } ) = ( ( N \ { K } ) i^i N )
103 3 83 4 27 102 gsmsymgreq 
 |-  ( ( ( ( N \ { K } ) e. Fin /\ N e. Fin ) /\ ( W e. Word ( Base ` S ) /\ U e. Word ( Base ` Z ) /\ ( # ` W ) = ( # ` U ) ) ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) -> A. n e. ( N \ { K } ) ( ( S gsum W ) ` n ) = ( ( Z gsum U ) ` n ) ) )
104 93 98 103 sylc 
 |-  ( ( -. k = K /\ ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) ) -> A. n e. ( N \ { K } ) ( ( S gsum W ) ` n ) = ( ( Z gsum U ) ` n ) )
105 67 anim2i 
 |-  ( ( k e. N /\ -. k = K ) -> ( k e. N /\ k =/= K ) )
106 105 69 sylibr 
 |-  ( ( k e. N /\ -. k = K ) -> k e. ( N \ { K } ) )
107 106 ex 
 |-  ( k e. N -> ( -. k = K -> k e. ( N \ { K } ) ) )
108 107 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) -> ( -. k = K -> k e. ( N \ { K } ) ) )
109 108 impcom 
 |-  ( ( -. k = K /\ ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) ) -> k e. ( N \ { K } ) )
110 78 104 109 rspcdva 
 |-  ( ( -. k = K /\ ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) ) -> ( ( S gsum W ) ` k ) = ( ( Z gsum U ) ` k ) )
111 65 75 110 3eqtr3d 
 |-  ( ( -. k = K /\ ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) ) -> ( Q ` k ) = ( ( Z gsum U ) ` k ) )
112 111 ex 
 |-  ( -. k = K -> ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) -> ( Q ` k ) = ( ( Z gsum U ) ` k ) ) )
113 61 112 pm2.61i 
 |-  ( ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) /\ k e. N ) -> ( Q ` k ) = ( ( Z gsum U ) ` k ) )
114 11 23 113 eqfnfvd 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) ) -> Q = ( Z gsum U ) )
115 114 exp31 
 |-  ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) -> ( ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) -> ( ( U e. Word R /\ ( # ` W ) = ( # ` U ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( U ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) ) -> Q = ( Z gsum U ) ) ) )