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