Metamath Proof Explorer

Theorem 2cshwcshw

Description: If a word is a cyclically shifted word, and a second word is the result of cyclically shifting the same word, then the second word is the result of cyclically shifting the first word. (Contributed by AV, 11-May-2018) (Revised by AV, 12-Jun-2018) (Proof shortened by AV, 3-Nov-2018)

Ref Expression
Assertion 2cshwcshw 
|- ( ( Y e. Word V /\ ( # ` Y ) = N ) -> ( ( K e. ( 0 ... N ) /\ X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) )

Proof

Step Hyp Ref Expression
1 difelfznle 
 |-  ( ( K e. ( 0 ... N ) /\ m e. ( 0 ... N ) /\ -. K <_ m ) -> ( ( m + N ) - K ) e. ( 0 ... N ) )
2 1 3exp 
 |-  ( K e. ( 0 ... N ) -> ( m e. ( 0 ... N ) -> ( -. K <_ m -> ( ( m + N ) - K ) e. ( 0 ... N ) ) ) )
3 2 ad2antrr 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) -> ( m e. ( 0 ... N ) -> ( -. K <_ m -> ( ( m + N ) - K ) e. ( 0 ... N ) ) ) )
4 3 imp 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) -> ( -. K <_ m -> ( ( m + N ) - K ) e. ( 0 ... N ) ) )
5 4 adantr 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) -> ( -. K <_ m -> ( ( m + N ) - K ) e. ( 0 ... N ) ) )
6 5 com12 
 |-  ( -. K <_ m -> ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) -> ( ( m + N ) - K ) e. ( 0 ... N ) ) )
7 6 adantl 
 |-  ( ( -. m = 0 /\ -. K <_ m ) -> ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) -> ( ( m + N ) - K ) e. ( 0 ... N ) ) )
8 7 imp 
 |-  ( ( ( -. m = 0 /\ -. K <_ m ) /\ ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) ) -> ( ( m + N ) - K ) e. ( 0 ... N ) )
9 simprl 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> Y e. Word V )
10 9 ad2antrr 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) -> Y e. Word V )
11 elfzelz 
 |-  ( K e. ( 0 ... N ) -> K e. ZZ )
12 11 adantr 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> K e. ZZ )
13 12 ad2antrr 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) -> K e. ZZ )
14 elfz2 
 |-  ( K e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( 0 <_ K /\ K <_ N ) ) )
15 zaddcl 
 |-  ( ( m e. ZZ /\ N e. ZZ ) -> ( m + N ) e. ZZ )
16 15 adantrr 
 |-  ( ( m e. ZZ /\ ( N e. ZZ /\ K e. ZZ ) ) -> ( m + N ) e. ZZ )
17 simprr 
 |-  ( ( m e. ZZ /\ ( N e. ZZ /\ K e. ZZ ) ) -> K e. ZZ )
18 16 17 zsubcld 
 |-  ( ( m e. ZZ /\ ( N e. ZZ /\ K e. ZZ ) ) -> ( ( m + N ) - K ) e. ZZ )
19 18 ex 
 |-  ( m e. ZZ -> ( ( N e. ZZ /\ K e. ZZ ) -> ( ( m + N ) - K ) e. ZZ ) )
20 elfzelz 
 |-  ( m e. ( 0 ... N ) -> m e. ZZ )
21 19 20 syl11 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( m e. ( 0 ... N ) -> ( ( m + N ) - K ) e. ZZ ) )
22 21 3adant1 
 |-  ( ( 0 e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( m e. ( 0 ... N ) -> ( ( m + N ) - K ) e. ZZ ) )
23 22 adantr 
 |-  ( ( ( 0 e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( 0 <_ K /\ K <_ N ) ) -> ( m e. ( 0 ... N ) -> ( ( m + N ) - K ) e. ZZ ) )
24 14 23 sylbi 
 |-  ( K e. ( 0 ... N ) -> ( m e. ( 0 ... N ) -> ( ( m + N ) - K ) e. ZZ ) )
25 24 ad2antrr 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) -> ( m e. ( 0 ... N ) -> ( ( m + N ) - K ) e. ZZ ) )
26 25 imp 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) -> ( ( m + N ) - K ) e. ZZ )
27 2cshw 
 |-  ( ( Y e. Word V /\ K e. ZZ /\ ( ( m + N ) - K ) e. ZZ ) -> ( ( Y cyclShift K ) cyclShift ( ( m + N ) - K ) ) = ( Y cyclShift ( K + ( ( m + N ) - K ) ) ) )
28 10 13 26 27 syl3anc 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) -> ( ( Y cyclShift K ) cyclShift ( ( m + N ) - K ) ) = ( Y cyclShift ( K + ( ( m + N ) - K ) ) ) )
29 17 18 zaddcld 
 |-  ( ( m e. ZZ /\ ( N e. ZZ /\ K e. ZZ ) ) -> ( K + ( ( m + N ) - K ) ) e. ZZ )
30 29 ex 
 |-  ( m e. ZZ -> ( ( N e. ZZ /\ K e. ZZ ) -> ( K + ( ( m + N ) - K ) ) e. ZZ ) )
31 30 20 syl11 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( m e. ( 0 ... N ) -> ( K + ( ( m + N ) - K ) ) e. ZZ ) )
32 31 3adant1 
 |-  ( ( 0 e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( m e. ( 0 ... N ) -> ( K + ( ( m + N ) - K ) ) e. ZZ ) )
33 32 adantr 
 |-  ( ( ( 0 e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( 0 <_ K /\ K <_ N ) ) -> ( m e. ( 0 ... N ) -> ( K + ( ( m + N ) - K ) ) e. ZZ ) )
34 14 33 sylbi 
 |-  ( K e. ( 0 ... N ) -> ( m e. ( 0 ... N ) -> ( K + ( ( m + N ) - K ) ) e. ZZ ) )
35 34 ad2antrr 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) -> ( m e. ( 0 ... N ) -> ( K + ( ( m + N ) - K ) ) e. ZZ ) )
36 35 imp 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) -> ( K + ( ( m + N ) - K ) ) e. ZZ )
37 cshwsublen 
 |-  ( ( Y e. Word V /\ ( K + ( ( m + N ) - K ) ) e. ZZ ) -> ( Y cyclShift ( K + ( ( m + N ) - K ) ) ) = ( Y cyclShift ( ( K + ( ( m + N ) - K ) ) - ( # ` Y ) ) ) )
38 10 36 37 syl2anc 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) -> ( Y cyclShift ( K + ( ( m + N ) - K ) ) ) = ( Y cyclShift ( ( K + ( ( m + N ) - K ) ) - ( # ` Y ) ) ) )
39 28 38 eqtrd 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) -> ( ( Y cyclShift K ) cyclShift ( ( m + N ) - K ) ) = ( Y cyclShift ( ( K + ( ( m + N ) - K ) ) - ( # ` Y ) ) ) )
40 elfz2nn0 
 |-  ( K e. ( 0 ... N ) <-> ( K e. NN0 /\ N e. NN0 /\ K <_ N ) )
41 nn0cn 
 |-  ( m e. NN0 -> m e. CC )
42 nn0cn 
 |-  ( K e. NN0 -> K e. CC )
43 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
44 42 43 anim12i 
 |-  ( ( K e. NN0 /\ N e. NN0 ) -> ( K e. CC /\ N e. CC ) )
45 simprl 
 |-  ( ( m e. CC /\ ( K e. CC /\ N e. CC ) ) -> K e. CC )
46 addcl 
 |-  ( ( m e. CC /\ N e. CC ) -> ( m + N ) e. CC )
47 46 adantrl 
 |-  ( ( m e. CC /\ ( K e. CC /\ N e. CC ) ) -> ( m + N ) e. CC )
48 45 47 pncan3d 
 |-  ( ( m e. CC /\ ( K e. CC /\ N e. CC ) ) -> ( K + ( ( m + N ) - K ) ) = ( m + N ) )
49 48 oveq1d 
 |-  ( ( m e. CC /\ ( K e. CC /\ N e. CC ) ) -> ( ( K + ( ( m + N ) - K ) ) - N ) = ( ( m + N ) - N ) )
50 pncan 
 |-  ( ( m e. CC /\ N e. CC ) -> ( ( m + N ) - N ) = m )
51 50 adantrl 
 |-  ( ( m e. CC /\ ( K e. CC /\ N e. CC ) ) -> ( ( m + N ) - N ) = m )
52 49 51 eqtrd 
 |-  ( ( m e. CC /\ ( K e. CC /\ N e. CC ) ) -> ( ( K + ( ( m + N ) - K ) ) - N ) = m )
53 41 44 52 syl2an 
 |-  ( ( m e. NN0 /\ ( K e. NN0 /\ N e. NN0 ) ) -> ( ( K + ( ( m + N ) - K ) ) - N ) = m )
54 53 ex 
 |-  ( m e. NN0 -> ( ( K e. NN0 /\ N e. NN0 ) -> ( ( K + ( ( m + N ) - K ) ) - N ) = m ) )
55 elfznn0 
 |-  ( m e. ( 0 ... N ) -> m e. NN0 )
56 54 55 syl11 
 |-  ( ( K e. NN0 /\ N e. NN0 ) -> ( m e. ( 0 ... N ) -> ( ( K + ( ( m + N ) - K ) ) - N ) = m ) )
57 56 3adant3 
 |-  ( ( K e. NN0 /\ N e. NN0 /\ K <_ N ) -> ( m e. ( 0 ... N ) -> ( ( K + ( ( m + N ) - K ) ) - N ) = m ) )
58 40 57 sylbi 
 |-  ( K e. ( 0 ... N ) -> ( m e. ( 0 ... N ) -> ( ( K + ( ( m + N ) - K ) ) - N ) = m ) )
59 58 adantr 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> ( m e. ( 0 ... N ) -> ( ( K + ( ( m + N ) - K ) ) - N ) = m ) )
60 oveq2 
 |-  ( ( # ` Y ) = N -> ( ( K + ( ( m + N ) - K ) ) - ( # ` Y ) ) = ( ( K + ( ( m + N ) - K ) ) - N ) )
61 60 eqeq1d 
 |-  ( ( # ` Y ) = N -> ( ( ( K + ( ( m + N ) - K ) ) - ( # ` Y ) ) = m <-> ( ( K + ( ( m + N ) - K ) ) - N ) = m ) )
62 61 imbi2d 
 |-  ( ( # ` Y ) = N -> ( ( m e. ( 0 ... N ) -> ( ( K + ( ( m + N ) - K ) ) - ( # ` Y ) ) = m ) <-> ( m e. ( 0 ... N ) -> ( ( K + ( ( m + N ) - K ) ) - N ) = m ) ) )
63 62 adantl 
 |-  ( ( Y e. Word V /\ ( # ` Y ) = N ) -> ( ( m e. ( 0 ... N ) -> ( ( K + ( ( m + N ) - K ) ) - ( # ` Y ) ) = m ) <-> ( m e. ( 0 ... N ) -> ( ( K + ( ( m + N ) - K ) ) - N ) = m ) ) )
64 63 adantl 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> ( ( m e. ( 0 ... N ) -> ( ( K + ( ( m + N ) - K ) ) - ( # ` Y ) ) = m ) <-> ( m e. ( 0 ... N ) -> ( ( K + ( ( m + N ) - K ) ) - N ) = m ) ) )
65 59 64 mpbird 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> ( m e. ( 0 ... N ) -> ( ( K + ( ( m + N ) - K ) ) - ( # ` Y ) ) = m ) )
66 65 adantr 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) -> ( m e. ( 0 ... N ) -> ( ( K + ( ( m + N ) - K ) ) - ( # ` Y ) ) = m ) )
67 66 imp 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) -> ( ( K + ( ( m + N ) - K ) ) - ( # ` Y ) ) = m )
68 67 oveq2d 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) -> ( Y cyclShift ( ( K + ( ( m + N ) - K ) ) - ( # ` Y ) ) ) = ( Y cyclShift m ) )
69 39 68 eqtr2d 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) -> ( Y cyclShift m ) = ( ( Y cyclShift K ) cyclShift ( ( m + N ) - K ) ) )
70 69 adantr 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) -> ( Y cyclShift m ) = ( ( Y cyclShift K ) cyclShift ( ( m + N ) - K ) ) )
71 oveq1 
 |-  ( X = ( Y cyclShift K ) -> ( X cyclShift ( ( m + N ) - K ) ) = ( ( Y cyclShift K ) cyclShift ( ( m + N ) - K ) ) )
72 71 adantl 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) -> ( X cyclShift ( ( m + N ) - K ) ) = ( ( Y cyclShift K ) cyclShift ( ( m + N ) - K ) ) )
73 70 72 eqtr4d 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) /\ m e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) -> ( Y cyclShift m ) = ( X cyclShift ( ( m + N ) - K ) ) )
74 73 exp41 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> ( ( -. m = 0 /\ -. K <_ m ) -> ( m e. ( 0 ... N ) -> ( X = ( Y cyclShift K ) -> ( Y cyclShift m ) = ( X cyclShift ( ( m + N ) - K ) ) ) ) ) )
75 74 com24 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> ( X = ( Y cyclShift K ) -> ( m e. ( 0 ... N ) -> ( ( -. m = 0 /\ -. K <_ m ) -> ( Y cyclShift m ) = ( X cyclShift ( ( m + N ) - K ) ) ) ) ) )
76 75 imp41 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) -> ( Y cyclShift m ) = ( X cyclShift ( ( m + N ) - K ) ) )
77 76 eqeq2d 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) -> ( Z = ( Y cyclShift m ) <-> Z = ( X cyclShift ( ( m + N ) - K ) ) ) )
78 77 biimpd 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ ( -. m = 0 /\ -. K <_ m ) ) -> ( Z = ( Y cyclShift m ) -> Z = ( X cyclShift ( ( m + N ) - K ) ) ) )
79 78 impancom 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) -> ( ( -. m = 0 /\ -. K <_ m ) -> Z = ( X cyclShift ( ( m + N ) - K ) ) ) )
80 79 impcom 
 |-  ( ( ( -. m = 0 /\ -. K <_ m ) /\ ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) ) -> Z = ( X cyclShift ( ( m + N ) - K ) ) )
81 oveq2 
 |-  ( n = ( ( m + N ) - K ) -> ( X cyclShift n ) = ( X cyclShift ( ( m + N ) - K ) ) )
82 81 rspceeqv 
 |-  ( ( ( ( m + N ) - K ) e. ( 0 ... N ) /\ Z = ( X cyclShift ( ( m + N ) - K ) ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) )
83 8 80 82 syl2anc 
 |-  ( ( ( -. m = 0 /\ -. K <_ m ) /\ ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) )
84 83 exp31 
 |-  ( -. m = 0 -> ( -. K <_ m -> ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) )
85 oveq2 
 |-  ( m = 0 -> ( Y cyclShift m ) = ( Y cyclShift 0 ) )
86 85 eqeq2d 
 |-  ( m = 0 -> ( Z = ( Y cyclShift m ) <-> Z = ( Y cyclShift 0 ) ) )
87 cshw0 
 |-  ( Y e. Word V -> ( Y cyclShift 0 ) = Y )
88 87 adantr 
 |-  ( ( Y e. Word V /\ ( # ` Y ) = N ) -> ( Y cyclShift 0 ) = Y )
89 88 eqeq2d 
 |-  ( ( Y e. Word V /\ ( # ` Y ) = N ) -> ( Z = ( Y cyclShift 0 ) <-> Z = Y ) )
90 fznn0sub2 
 |-  ( K e. ( 0 ... N ) -> ( N - K ) e. ( 0 ... N ) )
91 90 adantl 
 |-  ( ( ( Y e. Word V /\ ( # ` Y ) = N ) /\ K e. ( 0 ... N ) ) -> ( N - K ) e. ( 0 ... N ) )
92 oveq1 
 |-  ( ( # ` Y ) = N -> ( ( # ` Y ) - K ) = ( N - K ) )
93 92 eleq1d 
 |-  ( ( # ` Y ) = N -> ( ( ( # ` Y ) - K ) e. ( 0 ... N ) <-> ( N - K ) e. ( 0 ... N ) ) )
94 93 ad2antlr 
 |-  ( ( ( Y e. Word V /\ ( # ` Y ) = N ) /\ K e. ( 0 ... N ) ) -> ( ( ( # ` Y ) - K ) e. ( 0 ... N ) <-> ( N - K ) e. ( 0 ... N ) ) )
95 91 94 mpbird 
 |-  ( ( ( Y e. Word V /\ ( # ` Y ) = N ) /\ K e. ( 0 ... N ) ) -> ( ( # ` Y ) - K ) e. ( 0 ... N ) )
96 95 adantr 
 |-  ( ( ( ( Y e. Word V /\ ( # ` Y ) = N ) /\ K e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) -> ( ( # ` Y ) - K ) e. ( 0 ... N ) )
97 oveq1 
 |-  ( X = ( Y cyclShift K ) -> ( X cyclShift ( ( # ` Y ) - K ) ) = ( ( Y cyclShift K ) cyclShift ( ( # ` Y ) - K ) ) )
98 simpl 
 |-  ( ( Y e. Word V /\ ( # ` Y ) = N ) -> Y e. Word V )
99 2cshwid 
 |-  ( ( Y e. Word V /\ K e. ZZ ) -> ( ( Y cyclShift K ) cyclShift ( ( # ` Y ) - K ) ) = Y )
100 98 11 99 syl2an 
 |-  ( ( ( Y e. Word V /\ ( # ` Y ) = N ) /\ K e. ( 0 ... N ) ) -> ( ( Y cyclShift K ) cyclShift ( ( # ` Y ) - K ) ) = Y )
101 97 100 sylan9eqr 
 |-  ( ( ( ( Y e. Word V /\ ( # ` Y ) = N ) /\ K e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) -> ( X cyclShift ( ( # ` Y ) - K ) ) = Y )
102 101 eqcomd 
 |-  ( ( ( ( Y e. Word V /\ ( # ` Y ) = N ) /\ K e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) -> Y = ( X cyclShift ( ( # ` Y ) - K ) ) )
103 oveq2 
 |-  ( n = ( ( # ` Y ) - K ) -> ( X cyclShift n ) = ( X cyclShift ( ( # ` Y ) - K ) ) )
104 103 rspceeqv 
 |-  ( ( ( ( # ` Y ) - K ) e. ( 0 ... N ) /\ Y = ( X cyclShift ( ( # ` Y ) - K ) ) ) -> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) )
105 96 102 104 syl2anc 
 |-  ( ( ( ( Y e. Word V /\ ( # ` Y ) = N ) /\ K e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) -> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) )
106 105 adantr 
 |-  ( ( ( ( ( Y e. Word V /\ ( # ` Y ) = N ) /\ K e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) /\ Z = Y ) -> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) )
107 eqeq1 
 |-  ( Z = Y -> ( Z = ( X cyclShift n ) <-> Y = ( X cyclShift n ) ) )
108 107 rexbidv 
 |-  ( Z = Y -> ( E. n e. ( 0 ... N ) Z = ( X cyclShift n ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) )
109 108 adantl 
 |-  ( ( ( ( ( Y e. Word V /\ ( # ` Y ) = N ) /\ K e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) /\ Z = Y ) -> ( E. n e. ( 0 ... N ) Z = ( X cyclShift n ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) )
110 106 109 mpbird 
 |-  ( ( ( ( ( Y e. Word V /\ ( # ` Y ) = N ) /\ K e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) /\ Z = Y ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) )
111 110 exp41 
 |-  ( ( Y e. Word V /\ ( # ` Y ) = N ) -> ( K e. ( 0 ... N ) -> ( X = ( Y cyclShift K ) -> ( Z = Y -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) ) )
112 111 com24 
 |-  ( ( Y e. Word V /\ ( # ` Y ) = N ) -> ( Z = Y -> ( X = ( Y cyclShift K ) -> ( K e. ( 0 ... N ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) ) )
113 89 112 sylbid 
 |-  ( ( Y e. Word V /\ ( # ` Y ) = N ) -> ( Z = ( Y cyclShift 0 ) -> ( X = ( Y cyclShift K ) -> ( K e. ( 0 ... N ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) ) )
114 113 com24 
 |-  ( ( Y e. Word V /\ ( # ` Y ) = N ) -> ( K e. ( 0 ... N ) -> ( X = ( Y cyclShift K ) -> ( Z = ( Y cyclShift 0 ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) ) )
115 114 impcom 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> ( X = ( Y cyclShift K ) -> ( Z = ( Y cyclShift 0 ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) )
116 115 com13 
 |-  ( Z = ( Y cyclShift 0 ) -> ( X = ( Y cyclShift K ) -> ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) )
117 116 a1d 
 |-  ( Z = ( Y cyclShift 0 ) -> ( m e. ( 0 ... N ) -> ( X = ( Y cyclShift K ) -> ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) ) )
118 86 117 biimtrdi 
 |-  ( m = 0 -> ( Z = ( Y cyclShift m ) -> ( m e. ( 0 ... N ) -> ( X = ( Y cyclShift K ) -> ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) ) ) )
119 118 com24 
 |-  ( m = 0 -> ( X = ( Y cyclShift K ) -> ( m e. ( 0 ... N ) -> ( Z = ( Y cyclShift m ) -> ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) ) ) )
120 119 com15 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> ( X = ( Y cyclShift K ) -> ( m e. ( 0 ... N ) -> ( Z = ( Y cyclShift m ) -> ( m = 0 -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) ) ) )
121 120 imp41 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) -> ( m = 0 -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) )
122 121 com12 
 |-  ( m = 0 -> ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) )
123 difelfzle 
 |-  ( ( K e. ( 0 ... N ) /\ m e. ( 0 ... N ) /\ K <_ m ) -> ( m - K ) e. ( 0 ... N ) )
124 123 3exp 
 |-  ( K e. ( 0 ... N ) -> ( m e. ( 0 ... N ) -> ( K <_ m -> ( m - K ) e. ( 0 ... N ) ) ) )
125 124 ad2antrr 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) -> ( m e. ( 0 ... N ) -> ( K <_ m -> ( m - K ) e. ( 0 ... N ) ) ) )
126 125 imp 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) -> ( K <_ m -> ( m - K ) e. ( 0 ... N ) ) )
127 126 adantr 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) -> ( K <_ m -> ( m - K ) e. ( 0 ... N ) ) )
128 127 impcom 
 |-  ( ( K <_ m /\ ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) ) -> ( m - K ) e. ( 0 ... N ) )
129 9 ad2antrr 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) /\ m e. ( 0 ... N ) ) -> Y e. Word V )
130 12 ad2antrr 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) /\ m e. ( 0 ... N ) ) -> K e. ZZ )
131 zsubcl 
 |-  ( ( m e. ZZ /\ K e. ZZ ) -> ( m - K ) e. ZZ )
132 131 ex 
 |-  ( m e. ZZ -> ( K e. ZZ -> ( m - K ) e. ZZ ) )
133 20 11 132 syl2imc 
 |-  ( K e. ( 0 ... N ) -> ( m e. ( 0 ... N ) -> ( m - K ) e. ZZ ) )
134 133 ad2antrr 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) -> ( m e. ( 0 ... N ) -> ( m - K ) e. ZZ ) )
135 134 imp 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) /\ m e. ( 0 ... N ) ) -> ( m - K ) e. ZZ )
136 2cshw 
 |-  ( ( Y e. Word V /\ K e. ZZ /\ ( m - K ) e. ZZ ) -> ( ( Y cyclShift K ) cyclShift ( m - K ) ) = ( Y cyclShift ( K + ( m - K ) ) ) )
137 129 130 135 136 syl3anc 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) /\ m e. ( 0 ... N ) ) -> ( ( Y cyclShift K ) cyclShift ( m - K ) ) = ( Y cyclShift ( K + ( m - K ) ) ) )
138 zcn 
 |-  ( K e. ZZ -> K e. CC )
139 20 zcnd 
 |-  ( m e. ( 0 ... N ) -> m e. CC )
140 pncan3 
 |-  ( ( K e. CC /\ m e. CC ) -> ( K + ( m - K ) ) = m )
141 138 139 140 syl2anr 
 |-  ( ( m e. ( 0 ... N ) /\ K e. ZZ ) -> ( K + ( m - K ) ) = m )
142 141 ex 
 |-  ( m e. ( 0 ... N ) -> ( K e. ZZ -> ( K + ( m - K ) ) = m ) )
143 11 142 syl5com 
 |-  ( K e. ( 0 ... N ) -> ( m e. ( 0 ... N ) -> ( K + ( m - K ) ) = m ) )
144 143 ad2antrr 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) -> ( m e. ( 0 ... N ) -> ( K + ( m - K ) ) = m ) )
145 144 imp 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) /\ m e. ( 0 ... N ) ) -> ( K + ( m - K ) ) = m )
146 145 oveq2d 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) /\ m e. ( 0 ... N ) ) -> ( Y cyclShift ( K + ( m - K ) ) ) = ( Y cyclShift m ) )
147 137 146 eqtr2d 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) /\ m e. ( 0 ... N ) ) -> ( Y cyclShift m ) = ( ( Y cyclShift K ) cyclShift ( m - K ) ) )
148 147 adantr 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) /\ m e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) -> ( Y cyclShift m ) = ( ( Y cyclShift K ) cyclShift ( m - K ) ) )
149 oveq1 
 |-  ( X = ( Y cyclShift K ) -> ( X cyclShift ( m - K ) ) = ( ( Y cyclShift K ) cyclShift ( m - K ) ) )
150 149 eqeq2d 
 |-  ( X = ( Y cyclShift K ) -> ( ( Y cyclShift m ) = ( X cyclShift ( m - K ) ) <-> ( Y cyclShift m ) = ( ( Y cyclShift K ) cyclShift ( m - K ) ) ) )
151 150 adantl 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) /\ m e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) -> ( ( Y cyclShift m ) = ( X cyclShift ( m - K ) ) <-> ( Y cyclShift m ) = ( ( Y cyclShift K ) cyclShift ( m - K ) ) ) )
152 148 151 mpbird 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) /\ m e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) -> ( Y cyclShift m ) = ( X cyclShift ( m - K ) ) )
153 152 eqeq2d 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) /\ m e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) -> ( Z = ( Y cyclShift m ) <-> Z = ( X cyclShift ( m - K ) ) ) )
154 153 biimpd 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ K <_ m ) /\ m e. ( 0 ... N ) ) /\ X = ( Y cyclShift K ) ) -> ( Z = ( Y cyclShift m ) -> Z = ( X cyclShift ( m - K ) ) ) )
155 154 exp41 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> ( K <_ m -> ( m e. ( 0 ... N ) -> ( X = ( Y cyclShift K ) -> ( Z = ( Y cyclShift m ) -> Z = ( X cyclShift ( m - K ) ) ) ) ) ) )
156 155 com24 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> ( X = ( Y cyclShift K ) -> ( m e. ( 0 ... N ) -> ( K <_ m -> ( Z = ( Y cyclShift m ) -> Z = ( X cyclShift ( m - K ) ) ) ) ) ) )
157 156 imp31 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) -> ( K <_ m -> ( Z = ( Y cyclShift m ) -> Z = ( X cyclShift ( m - K ) ) ) ) )
158 157 com23 
 |-  ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) -> ( Z = ( Y cyclShift m ) -> ( K <_ m -> Z = ( X cyclShift ( m - K ) ) ) ) )
159 158 imp 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) -> ( K <_ m -> Z = ( X cyclShift ( m - K ) ) ) )
160 159 impcom 
 |-  ( ( K <_ m /\ ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) ) -> Z = ( X cyclShift ( m - K ) ) )
161 oveq2 
 |-  ( n = ( m - K ) -> ( X cyclShift n ) = ( X cyclShift ( m - K ) ) )
162 161 rspceeqv 
 |-  ( ( ( m - K ) e. ( 0 ... N ) /\ Z = ( X cyclShift ( m - K ) ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) )
163 128 160 162 syl2anc 
 |-  ( ( K <_ m /\ ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) )
164 163 ex 
 |-  ( K <_ m -> ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) )
165 84 122 164 pm2.61ii 
 |-  ( ( ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) /\ m e. ( 0 ... N ) ) /\ Z = ( Y cyclShift m ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) )
166 165 rexlimdva2 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) /\ X = ( Y cyclShift K ) ) -> ( E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) )
167 166 ex 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> ( X = ( Y cyclShift K ) -> ( E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) )
168 167 com23 
 |-  ( ( K e. ( 0 ... N ) /\ ( Y e. Word V /\ ( # ` Y ) = N ) ) -> ( E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) -> ( X = ( Y cyclShift K ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) )
169 168 ex 
 |-  ( K e. ( 0 ... N ) -> ( ( Y e. Word V /\ ( # ` Y ) = N ) -> ( E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) -> ( X = ( Y cyclShift K ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) ) )
170 169 com24 
 |-  ( K e. ( 0 ... N ) -> ( X = ( Y cyclShift K ) -> ( E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) -> ( ( Y e. Word V /\ ( # ` Y ) = N ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) ) ) )
171 170 3imp 
 |-  ( ( K e. ( 0 ... N ) /\ X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) -> ( ( Y e. Word V /\ ( # ` Y ) = N ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) )
172 171 com12 
 |-  ( ( Y e. Word V /\ ( # ` Y ) = N ) -> ( ( K e. ( 0 ... N ) /\ X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) )