Metamath Proof Explorer

Theorem psgndiflemA

Description: Lemma 2 for psgndif . (Contributed by AV, 31-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 psgndiflemA 
|- ( ( ( 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 ) -> ( Q = ( ( SymGrp ` N ) gsum U ) -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` 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 fveq2 
 |-  ( w = W -> ( # ` w ) = ( # ` W ) )
7 6 eqeq1d 
 |-  ( w = W -> ( ( # ` w ) = ( # ` r ) <-> ( # ` W ) = ( # ` r ) ) )
8 6 oveq2d 
 |-  ( w = W -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ ( # ` W ) ) )
9 fveq1 
 |-  ( w = W -> ( w ` i ) = ( W ` i ) )
10 9 fveq1d 
 |-  ( w = W -> ( ( w ` i ) ` n ) = ( ( W ` i ) ` n ) )
11 10 eqeq1d 
 |-  ( w = W -> ( ( ( w ` i ) ` n ) = ( ( r ` i ) ` n ) <-> ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) )
12 11 ralbidv 
 |-  ( w = W -> ( A. n e. ( N \ { K } ) ( ( w ` i ) ` n ) = ( ( r ` i ) ` n ) <-> A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) )
13 12 anbi2d 
 |-  ( w = W -> ( ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( w ` i ) ` n ) = ( ( r ` i ) ` n ) ) <-> ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) )
14 8 13 raleqbidv 
 |-  ( w = W -> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( w ` i ) ` n ) = ( ( r ` i ) ` n ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) )
15 7 14 anbi12d 
 |-  ( w = W -> ( ( ( # ` w ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( w ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) <-> ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) )
16 15 rexbidv 
 |-  ( w = W -> ( E. r e. Word R ( ( # ` w ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( w ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) <-> E. r e. Word R ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) )
17 16 rspccv 
 |-  ( A. w e. Word T E. r e. Word R ( ( # ` w ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( w ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) -> ( W e. Word T -> E. r e. Word R ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) )
18 2 5 pmtrdifwrdel2 
 |-  ( K e. N -> A. w e. Word T E. r e. Word R ( ( # ` w ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( w ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) )
19 17 18 syl11 
 |-  ( W e. Word T -> ( K e. N -> E. r e. Word R ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) )
20 19 3ad2ant1 
 |-  ( ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) /\ U e. Word R ) -> ( K e. N -> E. r e. Word R ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) )
21 20 com12 
 |-  ( K e. N -> ( ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) /\ U e. Word R ) -> E. r e. Word R ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) )
22 21 ad2antlr 
 |-  ( ( ( 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 ) -> E. r e. Word R ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) )
23 22 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 ) ) -> E. r e. Word R ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) )
24 oveq2 
 |-  ( ( # ` W ) = ( # ` r ) -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` r ) ) )
25 24 adantr 
 |-  ( ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` r ) ) )
26 25 ad3antlr 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` r ) ) )
27 simplll 
 |-  ( ( ( ( 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 ) ) -> N e. Fin )
28 27 ad2antlr 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> N e. Fin )
29 simplll 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> r e. Word R )
30 simprr3 
 |-  ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) -> U e. Word R )
31 30 adantr 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> U e. Word R )
32 simplrl 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) )
33 3simpa 
 |-  ( ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) /\ U e. Word R ) -> ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) )
34 33 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 e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) )
35 34 ad2antlr 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) )
36 simplrl 
 |-  ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) = ( # ` r ) )
37 36 adantr 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> ( # ` W ) = ( # ` r ) )
38 simplrr 
 |-  ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) )
39 38 adantr 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) )
40 1 2 3 4 5 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 ) ) -> ( ( r e. Word R /\ ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) -> Q = ( Z gsum r ) ) ) )
41 40 imp31 
 |-  ( ( ( ( ( N e. Fin /\ K e. N ) /\ Q e. { q e. P | ( q ` K ) = K } ) /\ ( W e. Word T /\ ( Q |` ( N \ { K } ) ) = ( S gsum W ) ) ) /\ ( r e. Word R /\ ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) -> Q = ( Z gsum r ) )
42 41 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 ) ) ) /\ ( r e. Word R /\ ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) -> ( Z gsum r ) = Q )
43 32 35 29 37 39 42 syl23anc 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> ( Z gsum r ) = Q )
44 id 
 |-  ( Q = ( ( SymGrp ` N ) gsum U ) -> Q = ( ( SymGrp ` N ) gsum U ) )
45 4 eqcomi 
 |-  ( SymGrp ` N ) = Z
46 45 oveq1i 
 |-  ( ( SymGrp ` N ) gsum U ) = ( Z gsum U )
47 44 46 eqtrdi 
 |-  ( Q = ( ( SymGrp ` N ) gsum U ) -> Q = ( Z gsum U ) )
48 47 adantl 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> Q = ( Z gsum U ) )
49 43 48 eqtrd 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> ( Z gsum r ) = ( Z gsum U ) )
50 4 5 28 29 31 49 psgnuni 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> ( -u 1 ^ ( # ` r ) ) = ( -u 1 ^ ( # ` U ) ) )
51 26 50 eqtrd 
 |-  ( ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) /\ Q = ( ( SymGrp ` N ) gsum U ) ) -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` U ) ) )
52 51 ex 
 |-  ( ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) /\ ( ( ( 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 ) ) ) -> ( Q = ( ( SymGrp ` N ) gsum U ) -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` U ) ) ) )
53 52 ex 
 |-  ( ( r e. Word R /\ ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) ) -> ( ( ( ( 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 ) ) -> ( Q = ( ( SymGrp ` N ) gsum U ) -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` U ) ) ) ) )
54 53 rexlimiva 
 |-  ( E. r e. Word R ( ( # ` W ) = ( # ` r ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( r ` i ) ` K ) = K /\ A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( r ` i ) ` n ) ) ) -> ( ( ( ( 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 ) ) -> ( Q = ( ( SymGrp ` N ) gsum U ) -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` U ) ) ) ) )
55 23 54 mpcom 
 |-  ( ( ( ( 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 ) ) -> ( Q = ( ( SymGrp ` N ) gsum U ) -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` U ) ) ) )
56 55 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 ) -> ( Q = ( ( SymGrp ` N ) gsum U ) -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` U ) ) ) ) )