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

Metamath Proof Explorer

Theorem cshwcsh2id

Description: A cyclically shifted word can be reconstructed by cyclically shifting it again twice. Lemma for erclwwlktr and erclwwlkntr . (Contributed by AV, 9-Apr-2018) (Revised by AV, 11-Jun-2018) (Proof shortened by AV, 3-Nov-2018)

Ref Expression
Hypotheses cshwcsh2id.1 
|- ( ph -> z e. Word V )
cshwcsh2id.2 
|- ( ph -> ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) )
Assertion cshwcsh2id 
|- ( ph -> ( ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )

Proof

Step Hyp Ref Expression
1 cshwcsh2id.1 
 |-  ( ph -> z e. Word V )
2 cshwcsh2id.2 
 |-  ( ph -> ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) )
3 oveq1 
 |-  ( y = ( z cyclShift k ) -> ( y cyclShift m ) = ( ( z cyclShift k ) cyclShift m ) )
4 3 eqeq2d 
 |-  ( y = ( z cyclShift k ) -> ( x = ( y cyclShift m ) <-> x = ( ( z cyclShift k ) cyclShift m ) ) )
5 4 anbi2d 
 |-  ( y = ( z cyclShift k ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) <-> ( m e. ( 0 ... ( # ` y ) ) /\ x = ( ( z cyclShift k ) cyclShift m ) ) ) )
6 5 adantr 
 |-  ( ( y = ( z cyclShift k ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) <-> ( m e. ( 0 ... ( # ` y ) ) /\ x = ( ( z cyclShift k ) cyclShift m ) ) ) )
7 elfznn0 
 |-  ( k e. ( 0 ... ( # ` z ) ) -> k e. NN0 )
8 elfznn0 
 |-  ( m e. ( 0 ... ( # ` y ) ) -> m e. NN0 )
9 nn0addcl 
 |-  ( ( k e. NN0 /\ m e. NN0 ) -> ( k + m ) e. NN0 )
10 7 8 9 syl2anr 
 |-  ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( k + m ) e. NN0 )
11 10 adantr 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( k + m ) e. NN0 )
12 elfz3nn0 
 |-  ( k e. ( 0 ... ( # ` z ) ) -> ( # ` z ) e. NN0 )
13 12 ad2antlr 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( # ` z ) e. NN0 )
14 simprl 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( k + m ) <_ ( # ` z ) )
15 elfz2nn0 
 |-  ( ( k + m ) e. ( 0 ... ( # ` z ) ) <-> ( ( k + m ) e. NN0 /\ ( # ` z ) e. NN0 /\ ( k + m ) <_ ( # ` z ) ) )
16 11 13 14 15 syl3anbrc 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( k + m ) e. ( 0 ... ( # ` z ) ) )
17 16 adantr 
 |-  ( ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( ( k + m ) <_ ( # ` z ) /\ ph ) ) /\ x = ( ( z cyclShift k ) cyclShift m ) ) -> ( k + m ) e. ( 0 ... ( # ` z ) ) )
18 1 adantl 
 |-  ( ( ( k + m ) <_ ( # ` z ) /\ ph ) -> z e. Word V )
19 18 adantl 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( ( k + m ) <_ ( # ` z ) /\ ph ) ) -> z e. Word V )
20 elfzelz 
 |-  ( k e. ( 0 ... ( # ` z ) ) -> k e. ZZ )
21 20 ad2antlr 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( ( k + m ) <_ ( # ` z ) /\ ph ) ) -> k e. ZZ )
22 elfzelz 
 |-  ( m e. ( 0 ... ( # ` y ) ) -> m e. ZZ )
23 22 adantr 
 |-  ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> m e. ZZ )
24 23 adantr 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( ( k + m ) <_ ( # ` z ) /\ ph ) ) -> m e. ZZ )
25 2cshw 
 |-  ( ( z e. Word V /\ k e. ZZ /\ m e. ZZ ) -> ( ( z cyclShift k ) cyclShift m ) = ( z cyclShift ( k + m ) ) )
26 19 21 24 25 syl3anc 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( ( z cyclShift k ) cyclShift m ) = ( z cyclShift ( k + m ) ) )
27 26 eqeq2d 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( x = ( ( z cyclShift k ) cyclShift m ) <-> x = ( z cyclShift ( k + m ) ) ) )
28 27 biimpa 
 |-  ( ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( ( k + m ) <_ ( # ` z ) /\ ph ) ) /\ x = ( ( z cyclShift k ) cyclShift m ) ) -> x = ( z cyclShift ( k + m ) ) )
29 17 28 jca 
 |-  ( ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( ( k + m ) <_ ( # ` z ) /\ ph ) ) /\ x = ( ( z cyclShift k ) cyclShift m ) ) -> ( ( k + m ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( k + m ) ) ) )
30 29 exp41 
 |-  ( m e. ( 0 ... ( # ` y ) ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( ( ( k + m ) <_ ( # ` z ) /\ ph ) -> ( x = ( ( z cyclShift k ) cyclShift m ) -> ( ( k + m ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( k + m ) ) ) ) ) ) )
31 30 com23 
 |-  ( m e. ( 0 ... ( # ` y ) ) -> ( ( ( k + m ) <_ ( # ` z ) /\ ph ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( x = ( ( z cyclShift k ) cyclShift m ) -> ( ( k + m ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( k + m ) ) ) ) ) ) )
32 31 com24 
 |-  ( m e. ( 0 ... ( # ` y ) ) -> ( x = ( ( z cyclShift k ) cyclShift m ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( ( ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( k + m ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( k + m ) ) ) ) ) ) )
33 32 imp 
 |-  ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( ( z cyclShift k ) cyclShift m ) ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( ( ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( k + m ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( k + m ) ) ) ) ) )
34 33 com12 
 |-  ( k e. ( 0 ... ( # ` z ) ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( ( z cyclShift k ) cyclShift m ) ) -> ( ( ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( k + m ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( k + m ) ) ) ) ) )
35 34 adantl 
 |-  ( ( y = ( z cyclShift k ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( ( z cyclShift k ) cyclShift m ) ) -> ( ( ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( k + m ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( k + m ) ) ) ) ) )
36 6 35 sylbid 
 |-  ( ( y = ( z cyclShift k ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) -> ( ( ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( k + m ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( k + m ) ) ) ) ) )
37 36 ancoms 
 |-  ( ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) -> ( ( ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( k + m ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( k + m ) ) ) ) ) )
38 37 impcom 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) -> ( ( ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( k + m ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( k + m ) ) ) ) )
39 oveq2 
 |-  ( n = ( k + m ) -> ( z cyclShift n ) = ( z cyclShift ( k + m ) ) )
40 39 rspceeqv 
 |-  ( ( ( k + m ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( k + m ) ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) )
41 38 40 syl6com 
 |-  ( ( ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
42 elfz2 
 |-  ( k e. ( 0 ... ( # ` z ) ) <-> ( ( 0 e. ZZ /\ ( # ` z ) e. ZZ /\ k e. ZZ ) /\ ( 0 <_ k /\ k <_ ( # ` z ) ) ) )
43 nn0z 
 |-  ( m e. NN0 -> m e. ZZ )
44 zaddcl 
 |-  ( ( k e. ZZ /\ m e. ZZ ) -> ( k + m ) e. ZZ )
45 44 ex 
 |-  ( k e. ZZ -> ( m e. ZZ -> ( k + m ) e. ZZ ) )
46 45 adantl 
 |-  ( ( ( # ` z ) e. ZZ /\ k e. ZZ ) -> ( m e. ZZ -> ( k + m ) e. ZZ ) )
47 46 impcom 
 |-  ( ( m e. ZZ /\ ( ( # ` z ) e. ZZ /\ k e. ZZ ) ) -> ( k + m ) e. ZZ )
48 simprl 
 |-  ( ( m e. ZZ /\ ( ( # ` z ) e. ZZ /\ k e. ZZ ) ) -> ( # ` z ) e. ZZ )
49 47 48 zsubcld 
 |-  ( ( m e. ZZ /\ ( ( # ` z ) e. ZZ /\ k e. ZZ ) ) -> ( ( k + m ) - ( # ` z ) ) e. ZZ )
50 49 ex 
 |-  ( m e. ZZ -> ( ( ( # ` z ) e. ZZ /\ k e. ZZ ) -> ( ( k + m ) - ( # ` z ) ) e. ZZ ) )
51 43 50 syl 
 |-  ( m e. NN0 -> ( ( ( # ` z ) e. ZZ /\ k e. ZZ ) -> ( ( k + m ) - ( # ` z ) ) e. ZZ ) )
52 51 com12 
 |-  ( ( ( # ` z ) e. ZZ /\ k e. ZZ ) -> ( m e. NN0 -> ( ( k + m ) - ( # ` z ) ) e. ZZ ) )
53 52 3adant1 
 |-  ( ( 0 e. ZZ /\ ( # ` z ) e. ZZ /\ k e. ZZ ) -> ( m e. NN0 -> ( ( k + m ) - ( # ` z ) ) e. ZZ ) )
54 53 adantr 
 |-  ( ( ( 0 e. ZZ /\ ( # ` z ) e. ZZ /\ k e. ZZ ) /\ ( 0 <_ k /\ k <_ ( # ` z ) ) ) -> ( m e. NN0 -> ( ( k + m ) - ( # ` z ) ) e. ZZ ) )
55 42 54 sylbi 
 |-  ( k e. ( 0 ... ( # ` z ) ) -> ( m e. NN0 -> ( ( k + m ) - ( # ` z ) ) e. ZZ ) )
56 8 55 mpan9 
 |-  ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( ( k + m ) - ( # ` z ) ) e. ZZ )
57 56 adantr 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( ( k + m ) - ( # ` z ) ) e. ZZ )
58 elfz2nn0 
 |-  ( k e. ( 0 ... ( # ` z ) ) <-> ( k e. NN0 /\ ( # ` z ) e. NN0 /\ k <_ ( # ` z ) ) )
59 nn0re 
 |-  ( k e. NN0 -> k e. RR )
60 nn0re 
 |-  ( ( # ` z ) e. NN0 -> ( # ` z ) e. RR )
61 59 60 anim12i 
 |-  ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) -> ( k e. RR /\ ( # ` z ) e. RR ) )
62 nn0re 
 |-  ( m e. NN0 -> m e. RR )
63 61 62 anim12i 
 |-  ( ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) /\ m e. NN0 ) -> ( ( k e. RR /\ ( # ` z ) e. RR ) /\ m e. RR ) )
64 simplr 
 |-  ( ( ( k e. RR /\ ( # ` z ) e. RR ) /\ m e. RR ) -> ( # ` z ) e. RR )
65 readdcl 
 |-  ( ( k e. RR /\ m e. RR ) -> ( k + m ) e. RR )
66 65 adantlr 
 |-  ( ( ( k e. RR /\ ( # ` z ) e. RR ) /\ m e. RR ) -> ( k + m ) e. RR )
67 64 66 ltnled 
 |-  ( ( ( k e. RR /\ ( # ` z ) e. RR ) /\ m e. RR ) -> ( ( # ` z ) < ( k + m ) <-> -. ( k + m ) <_ ( # ` z ) ) )
68 64 66 posdifd 
 |-  ( ( ( k e. RR /\ ( # ` z ) e. RR ) /\ m e. RR ) -> ( ( # ` z ) < ( k + m ) <-> 0 < ( ( k + m ) - ( # ` z ) ) ) )
69 68 biimpd 
 |-  ( ( ( k e. RR /\ ( # ` z ) e. RR ) /\ m e. RR ) -> ( ( # ` z ) < ( k + m ) -> 0 < ( ( k + m ) - ( # ` z ) ) ) )
70 67 69 sylbird 
 |-  ( ( ( k e. RR /\ ( # ` z ) e. RR ) /\ m e. RR ) -> ( -. ( k + m ) <_ ( # ` z ) -> 0 < ( ( k + m ) - ( # ` z ) ) ) )
71 63 70 syl 
 |-  ( ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) /\ m e. NN0 ) -> ( -. ( k + m ) <_ ( # ` z ) -> 0 < ( ( k + m ) - ( # ` z ) ) ) )
72 71 ex 
 |-  ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) -> ( m e. NN0 -> ( -. ( k + m ) <_ ( # ` z ) -> 0 < ( ( k + m ) - ( # ` z ) ) ) ) )
73 72 3adant3 
 |-  ( ( k e. NN0 /\ ( # ` z ) e. NN0 /\ k <_ ( # ` z ) ) -> ( m e. NN0 -> ( -. ( k + m ) <_ ( # ` z ) -> 0 < ( ( k + m ) - ( # ` z ) ) ) ) )
74 58 73 sylbi 
 |-  ( k e. ( 0 ... ( # ` z ) ) -> ( m e. NN0 -> ( -. ( k + m ) <_ ( # ` z ) -> 0 < ( ( k + m ) - ( # ` z ) ) ) ) )
75 8 74 mpan9 
 |-  ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( -. ( k + m ) <_ ( # ` z ) -> 0 < ( ( k + m ) - ( # ` z ) ) ) )
76 75 com12 
 |-  ( -. ( k + m ) <_ ( # ` z ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> 0 < ( ( k + m ) - ( # ` z ) ) ) )
77 76 adantr 
 |-  ( ( -. ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> 0 < ( ( k + m ) - ( # ` z ) ) ) )
78 77 impcom 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> 0 < ( ( k + m ) - ( # ` z ) ) )
79 elnnz 
 |-  ( ( ( k + m ) - ( # ` z ) ) e. NN <-> ( ( ( k + m ) - ( # ` z ) ) e. ZZ /\ 0 < ( ( k + m ) - ( # ` z ) ) ) )
80 57 78 79 sylanbrc 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( ( k + m ) - ( # ` z ) ) e. NN )
81 80 nnnn0d 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( ( k + m ) - ( # ` z ) ) e. NN0 )
82 12 ad2antlr 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( # ` z ) e. NN0 )
83 oveq2 
 |-  ( ( # ` y ) = ( # ` z ) -> ( 0 ... ( # ` y ) ) = ( 0 ... ( # ` z ) ) )
84 83 eleq2d 
 |-  ( ( # ` y ) = ( # ` z ) -> ( m e. ( 0 ... ( # ` y ) ) <-> m e. ( 0 ... ( # ` z ) ) ) )
85 84 anbi1d 
 |-  ( ( # ` y ) = ( # ` z ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) <-> ( m e. ( 0 ... ( # ` z ) ) /\ k e. ( 0 ... ( # ` z ) ) ) ) )
86 elfz2nn0 
 |-  ( m e. ( 0 ... ( # ` z ) ) <-> ( m e. NN0 /\ ( # ` z ) e. NN0 /\ m <_ ( # ` z ) ) )
87 59 adantr 
 |-  ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) -> k e. RR )
88 87 62 anim12i 
 |-  ( ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) /\ m e. NN0 ) -> ( k e. RR /\ m e. RR ) )
89 60 60 jca 
 |-  ( ( # ` z ) e. NN0 -> ( ( # ` z ) e. RR /\ ( # ` z ) e. RR ) )
90 89 ad2antlr 
 |-  ( ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) /\ m e. NN0 ) -> ( ( # ` z ) e. RR /\ ( # ` z ) e. RR ) )
91 le2add 
 |-  ( ( ( k e. RR /\ m e. RR ) /\ ( ( # ` z ) e. RR /\ ( # ` z ) e. RR ) ) -> ( ( k <_ ( # ` z ) /\ m <_ ( # ` z ) ) -> ( k + m ) <_ ( ( # ` z ) + ( # ` z ) ) ) )
92 88 90 91 syl2anc 
 |-  ( ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) /\ m e. NN0 ) -> ( ( k <_ ( # ` z ) /\ m <_ ( # ` z ) ) -> ( k + m ) <_ ( ( # ` z ) + ( # ` z ) ) ) )
93 nn0readdcl 
 |-  ( ( k e. NN0 /\ m e. NN0 ) -> ( k + m ) e. RR )
94 93 adantlr 
 |-  ( ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) /\ m e. NN0 ) -> ( k + m ) e. RR )
95 60 ad2antlr 
 |-  ( ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) /\ m e. NN0 ) -> ( # ` z ) e. RR )
96 94 95 95 lesubadd2d 
 |-  ( ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) /\ m e. NN0 ) -> ( ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) <-> ( k + m ) <_ ( ( # ` z ) + ( # ` z ) ) ) )
97 92 96 sylibrd 
 |-  ( ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) /\ m e. NN0 ) -> ( ( k <_ ( # ` z ) /\ m <_ ( # ` z ) ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) )
98 97 expcomd 
 |-  ( ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) /\ m e. NN0 ) -> ( m <_ ( # ` z ) -> ( k <_ ( # ` z ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) ) )
99 98 ex 
 |-  ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) -> ( m e. NN0 -> ( m <_ ( # ` z ) -> ( k <_ ( # ` z ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) ) ) )
100 99 com24 
 |-  ( ( k e. NN0 /\ ( # ` z ) e. NN0 ) -> ( k <_ ( # ` z ) -> ( m <_ ( # ` z ) -> ( m e. NN0 -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) ) ) )
101 100 3impia 
 |-  ( ( k e. NN0 /\ ( # ` z ) e. NN0 /\ k <_ ( # ` z ) ) -> ( m <_ ( # ` z ) -> ( m e. NN0 -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) ) )
102 101 com13 
 |-  ( m e. NN0 -> ( m <_ ( # ` z ) -> ( ( k e. NN0 /\ ( # ` z ) e. NN0 /\ k <_ ( # ` z ) ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) ) )
103 102 imp 
 |-  ( ( m e. NN0 /\ m <_ ( # ` z ) ) -> ( ( k e. NN0 /\ ( # ` z ) e. NN0 /\ k <_ ( # ` z ) ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) )
104 58 103 biimtrid 
 |-  ( ( m e. NN0 /\ m <_ ( # ` z ) ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) )
105 104 3adant2 
 |-  ( ( m e. NN0 /\ ( # ` z ) e. NN0 /\ m <_ ( # ` z ) ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) )
106 86 105 sylbi 
 |-  ( m e. ( 0 ... ( # ` z ) ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) )
107 106 imp 
 |-  ( ( m e. ( 0 ... ( # ` z ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) )
108 85 107 biimtrdi 
 |-  ( ( # ` y ) = ( # ` z ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) )
109 108 adantr 
 |-  ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) )
110 2 109 syl 
 |-  ( ph -> ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) )
111 110 adantl 
 |-  ( ( -. ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) )
112 111 impcom 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) )
113 elfz2nn0 
 |-  ( ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) <-> ( ( ( k + m ) - ( # ` z ) ) e. NN0 /\ ( # ` z ) e. NN0 /\ ( ( k + m ) - ( # ` z ) ) <_ ( # ` z ) ) )
114 81 82 112 113 syl3anbrc 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) )
115 114 adantr 
 |-  ( ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) /\ x = ( ( z cyclShift k ) cyclShift m ) ) -> ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) )
116 1 adantl 
 |-  ( ( -. ( k + m ) <_ ( # ` z ) /\ ph ) -> z e. Word V )
117 116 adantl 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> z e. Word V )
118 20 ad2antlr 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> k e. ZZ )
119 23 adantr 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> m e. ZZ )
120 117 118 119 25 syl3anc 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( ( z cyclShift k ) cyclShift m ) = ( z cyclShift ( k + m ) ) )
121 20 22 44 syl2anr 
 |-  ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( k + m ) e. ZZ )
122 cshwsublen 
 |-  ( ( z e. Word V /\ ( k + m ) e. ZZ ) -> ( z cyclShift ( k + m ) ) = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) )
123 116 121 122 syl2anr 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( z cyclShift ( k + m ) ) = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) )
124 120 123 eqtrd 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( ( z cyclShift k ) cyclShift m ) = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) )
125 124 eqeq2d 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) -> ( x = ( ( z cyclShift k ) cyclShift m ) <-> x = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) ) )
126 125 biimpa 
 |-  ( ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) /\ x = ( ( z cyclShift k ) cyclShift m ) ) -> x = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) )
127 115 126 jca 
 |-  ( ( ( ( m e. ( 0 ... ( # ` y ) ) /\ k e. ( 0 ... ( # ` z ) ) ) /\ ( -. ( k + m ) <_ ( # ` z ) /\ ph ) ) /\ x = ( ( z cyclShift k ) cyclShift m ) ) -> ( ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) ) )
128 127 exp41 
 |-  ( m e. ( 0 ... ( # ` y ) ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( ( -. ( k + m ) <_ ( # ` z ) /\ ph ) -> ( x = ( ( z cyclShift k ) cyclShift m ) -> ( ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) ) ) ) ) )
129 128 com23 
 |-  ( m e. ( 0 ... ( # ` y ) ) -> ( ( -. ( k + m ) <_ ( # ` z ) /\ ph ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( x = ( ( z cyclShift k ) cyclShift m ) -> ( ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) ) ) ) ) )
130 129 com24 
 |-  ( m e. ( 0 ... ( # ` y ) ) -> ( x = ( ( z cyclShift k ) cyclShift m ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( ( -. ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) ) ) ) ) )
131 130 imp 
 |-  ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( ( z cyclShift k ) cyclShift m ) ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( ( -. ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) ) ) ) )
132 5 131 biimtrdi 
 |-  ( y = ( z cyclShift k ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( ( -. ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) ) ) ) ) )
133 132 com23 
 |-  ( y = ( z cyclShift k ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) -> ( ( -. ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) ) ) ) ) )
134 133 impcom 
 |-  ( ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) -> ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) -> ( ( -. ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) ) ) ) )
135 134 impcom 
 |-  ( ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) -> ( ( -. ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) ) ) )
136 oveq2 
 |-  ( n = ( ( k + m ) - ( # ` z ) ) -> ( z cyclShift n ) = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) )
137 136 rspceeqv 
 |-  ( ( ( ( k + m ) - ( # ` z ) ) e. ( 0 ... ( # ` z ) ) /\ x = ( z cyclShift ( ( k + m ) - ( # ` z ) ) ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) )
138 135 137 syl6com 
 |-  ( ( -. ( k + m ) <_ ( # ` z ) /\ ph ) -> ( ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
139 41 138 pm2.61ian 
 |-  ( ph -> ( ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )