# 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 syl6bi
` |-  ( 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 ) ) )`