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 Word V Y = N K 0 N X = Y cyclShift K m 0 N Z = Y cyclShift m n 0 N Z = X cyclShift n

Proof

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