Metamath Proof Explorer


Theorem cshw1

Description: If cyclically shifting a word by 1 position results in the word itself, the word is build of identical symbols. Remark: also "valid" for an empty word! (Contributed by AV, 13-May-2018) (Revised by AV, 7-Jun-2018) (Proof shortened by AV, 1-Nov-2018)

Ref Expression
Assertion cshw1 W Word V W cyclShift 1 = W i 0 ..^ W W i = W 0

Proof

Step Hyp Ref Expression
1 ral0 i W i = W 0
2 oveq2 W = 0 0 ..^ W = 0 ..^ 0
3 fzo0 0 ..^ 0 =
4 2 3 eqtrdi W = 0 0 ..^ W =
5 4 raleqdv W = 0 i 0 ..^ W W i = W 0 i W i = W 0
6 1 5 mpbiri W = 0 i 0 ..^ W W i = W 0
7 6 a1d W = 0 W Word V W cyclShift 1 = W i 0 ..^ W W i = W 0
8 simprl ¬ W = 0 ¬ W = 1 W Word V W cyclShift 1 = W W Word V
9 lencl W Word V W 0
10 1nn0 1 0
11 10 a1i W 0 ¬ W = 0 ¬ W = 1 1 0
12 df-ne W 0 ¬ W = 0
13 elnnne0 W W 0 W 0
14 13 simplbi2com W 0 W 0 W
15 12 14 sylbir ¬ W = 0 W 0 W
16 15 adantr ¬ W = 0 ¬ W = 1 W 0 W
17 16 impcom W 0 ¬ W = 0 ¬ W = 1 W
18 neqne ¬ W = 1 W 1
19 18 ad2antll W 0 ¬ W = 0 ¬ W = 1 W 1
20 nngt1ne1 W 1 < W W 1
21 17 20 syl W 0 ¬ W = 0 ¬ W = 1 1 < W W 1
22 19 21 mpbird W 0 ¬ W = 0 ¬ W = 1 1 < W
23 elfzo0 1 0 ..^ W 1 0 W 1 < W
24 11 17 22 23 syl3anbrc W 0 ¬ W = 0 ¬ W = 1 1 0 ..^ W
25 24 ex W 0 ¬ W = 0 ¬ W = 1 1 0 ..^ W
26 9 25 syl W Word V ¬ W = 0 ¬ W = 1 1 0 ..^ W
27 26 adantr W Word V W cyclShift 1 = W ¬ W = 0 ¬ W = 1 1 0 ..^ W
28 27 impcom ¬ W = 0 ¬ W = 1 W Word V W cyclShift 1 = W 1 0 ..^ W
29 simprr ¬ W = 0 ¬ W = 1 W Word V W cyclShift 1 = W W cyclShift 1 = W
30 lbfzo0 0 0 ..^ W W
31 30 13 sylbbr W 0 W 0 0 0 ..^ W
32 31 ex W 0 W 0 0 0 ..^ W
33 12 32 syl5bir W 0 ¬ W = 0 0 0 ..^ W
34 9 33 syl W Word V ¬ W = 0 0 0 ..^ W
35 34 adantr W Word V W cyclShift 1 = W ¬ W = 0 0 0 ..^ W
36 35 com12 ¬ W = 0 W Word V W cyclShift 1 = W 0 0 ..^ W
37 36 adantr ¬ W = 0 ¬ W = 1 W Word V W cyclShift 1 = W 0 0 ..^ W
38 37 imp ¬ W = 0 ¬ W = 1 W Word V W cyclShift 1 = W 0 0 ..^ W
39 elfzoelz 1 0 ..^ W 1
40 cshweqrep W Word V 1 W cyclShift 1 = W 0 0 ..^ W i 0 W 0 = W 0 + i 1 mod W
41 39 40 sylan2 W Word V 1 0 ..^ W W cyclShift 1 = W 0 0 ..^ W i 0 W 0 = W 0 + i 1 mod W
42 41 imp W Word V 1 0 ..^ W W cyclShift 1 = W 0 0 ..^ W i 0 W 0 = W 0 + i 1 mod W
43 8 28 29 38 42 syl22anc ¬ W = 0 ¬ W = 1 W Word V W cyclShift 1 = W i 0 W 0 = W 0 + i 1 mod W
44 0nn0 0 0
45 fzossnn0 0 0 0 ..^ W 0
46 ssralv 0 ..^ W 0 i 0 W 0 = W 0 + i 1 mod W i 0 ..^ W W 0 = W 0 + i 1 mod W
47 44 45 46 mp2b i 0 W 0 = W 0 + i 1 mod W i 0 ..^ W W 0 = W 0 + i 1 mod W
48 eqcom W 0 = W 0 + i 1 mod W W 0 + i 1 mod W = W 0
49 elfzoelz i 0 ..^ W i
50 zre i i
51 ax-1rid i i 1 = i
52 50 51 syl i i 1 = i
53 52 oveq2d i 0 + i 1 = 0 + i
54 zcn i i
55 54 addid2d i 0 + i = i
56 53 55 eqtrd i 0 + i 1 = i
57 49 56 syl i 0 ..^ W 0 + i 1 = i
58 57 oveq1d i 0 ..^ W 0 + i 1 mod W = i mod W
59 zmodidfzoimp i 0 ..^ W i mod W = i
60 58 59 eqtrd i 0 ..^ W 0 + i 1 mod W = i
61 60 fveqeq2d i 0 ..^ W W 0 + i 1 mod W = W 0 W i = W 0
62 61 biimpd i 0 ..^ W W 0 + i 1 mod W = W 0 W i = W 0
63 48 62 syl5bi i 0 ..^ W W 0 = W 0 + i 1 mod W W i = W 0
64 63 ralimia i 0 ..^ W W 0 = W 0 + i 1 mod W i 0 ..^ W W i = W 0
65 47 64 syl i 0 W 0 = W 0 + i 1 mod W i 0 ..^ W W i = W 0
66 43 65 syl ¬ W = 0 ¬ W = 1 W Word V W cyclShift 1 = W i 0 ..^ W W i = W 0
67 66 ex ¬ W = 0 ¬ W = 1 W Word V W cyclShift 1 = W i 0 ..^ W W i = W 0
68 67 impancom ¬ W = 0 W Word V W cyclShift 1 = W ¬ W = 1 i 0 ..^ W W i = W 0
69 eqid W 0 = W 0
70 c0ex 0 V
71 fveqeq2 i = 0 W i = W 0 W 0 = W 0
72 70 71 ralsn i 0 W i = W 0 W 0 = W 0
73 69 72 mpbir i 0 W i = W 0
74 oveq2 W = 1 0 ..^ W = 0 ..^ 1
75 fzo01 0 ..^ 1 = 0
76 74 75 eqtrdi W = 1 0 ..^ W = 0
77 76 raleqdv W = 1 i 0 ..^ W W i = W 0 i 0 W i = W 0
78 73 77 mpbiri W = 1 i 0 ..^ W W i = W 0
79 68 78 pm2.61d2 ¬ W = 0 W Word V W cyclShift 1 = W i 0 ..^ W W i = W 0
80 79 ex ¬ W = 0 W Word V W cyclShift 1 = W i 0 ..^ W W i = W 0
81 7 80 pm2.61i W Word V W cyclShift 1 = W i 0 ..^ W W i = W 0