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∈WordV∧WcyclShift1=W→∀i∈0..^WW⁡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..^WW⁡i=W⁡0↔∀i∈∅W⁡i=W⁡0
6 1 5 mpbiri ⊢W=0→∀i∈0..^WW⁡i=W⁡0
7 6 a1d ⊢W=0→W∈WordV∧WcyclShift1=W→∀i∈0..^WW⁡i=W⁡0
8 simprl ⊢¬W=0∧¬W=1∧W∈WordV∧WcyclShift1=W→W∈WordV
9 lencl ⊢W∈WordV→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∈WordV→¬W=0∧¬W=1→1∈0..^W
27 26 adantr ⊢W∈WordV∧WcyclShift1=W→¬W=0∧¬W=1→1∈0..^W
28 27 impcom ⊢¬W=0∧¬W=1∧W∈WordV∧WcyclShift1=W→1∈0..^W
29 simprr ⊢¬W=0∧¬W=1∧W∈WordV∧WcyclShift1=W→WcyclShift1=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 biimtrrid ⊢W∈ℕ0→¬W=0→0∈0..^W
34 9 33 syl ⊢W∈WordV→¬W=0→0∈0..^W
35 34 adantr ⊢W∈WordV∧WcyclShift1=W→¬W=0→0∈0..^W
36 35 com12 ⊢¬W=0→W∈WordV∧WcyclShift1=W→0∈0..^W
37 36 adantr ⊢¬W=0∧¬W=1→W∈WordV∧WcyclShift1=W→0∈0..^W
38 37 imp ⊢¬W=0∧¬W=1∧W∈WordV∧WcyclShift1=W→0∈0..^W
39 elfzoelz ⊢1∈0..^W→1∈ℤ
40 cshweqrep ⊢W∈WordV∧1∈ℤ→WcyclShift1=W∧0∈0..^W→∀i∈ℕ0W⁡0=W⁡0+i⋅1modW
41 39 40 sylan2 ⊢W∈WordV∧1∈0..^W→WcyclShift1=W∧0∈0..^W→∀i∈ℕ0W⁡0=W⁡0+i⋅1modW
42 41 imp ⊢W∈WordV∧1∈0..^W∧WcyclShift1=W∧0∈0..^W→∀i∈ℕ0W⁡0=W⁡0+i⋅1modW
43 8 28 29 38 42 syl22anc ⊢¬W=0∧¬W=1∧W∈WordV∧WcyclShift1=W→∀i∈ℕ0W⁡0=W⁡0+i⋅1modW
44 0nn0 ⊢0∈ℕ0
45 fzossnn0 ⊢0∈ℕ0→0..^W⊆ℕ0
46 ssralv ⊢0..^W⊆ℕ0→∀i∈ℕ0W⁡0=W⁡0+i⋅1modW→∀i∈0..^WW⁡0=W⁡0+i⋅1modW
47 44 45 46 mp2b ⊢∀i∈ℕ0W⁡0=W⁡0+i⋅1modW→∀i∈0..^WW⁡0=W⁡0+i⋅1modW
48 eqcom ⊢W⁡0=W⁡0+i⋅1modW↔W⁡0+i⋅1modW=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 addlidd ⊢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⋅1modW=imodW
59 zmodidfzoimp ⊢i∈0..^W→imodW=i
60 58 59 eqtrd ⊢i∈0..^W→0+i⋅1modW=i
61 60 fveqeq2d ⊢i∈0..^W→W⁡0+i⋅1modW=W⁡0↔W⁡i=W⁡0
62 61 biimpd ⊢i∈0..^W→W⁡0+i⋅1modW=W⁡0→W⁡i=W⁡0
63 48 62 biimtrid ⊢i∈0..^W→W⁡0=W⁡0+i⋅1modW→W⁡i=W⁡0
64 63 ralimia ⊢∀i∈0..^WW⁡0=W⁡0+i⋅1modW→∀i∈0..^WW⁡i=W⁡0
65 47 64 syl ⊢∀i∈ℕ0W⁡0=W⁡0+i⋅1modW→∀i∈0..^WW⁡i=W⁡0
66 43 65 syl ⊢¬W=0∧¬W=1∧W∈WordV∧WcyclShift1=W→∀i∈0..^WW⁡i=W⁡0
67 66 ex ⊢¬W=0∧¬W=1→W∈WordV∧WcyclShift1=W→∀i∈0..^WW⁡i=W⁡0
68 67 impancom ⊢¬W=0∧W∈WordV∧WcyclShift1=W→¬W=1→∀i∈0..^WW⁡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∈0W⁡i=W⁡0↔W⁡0=W⁡0
73 69 72 mpbir ⊢∀i∈0W⁡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..^WW⁡i=W⁡0↔∀i∈0W⁡i=W⁡0
78 73 77 mpbiri ⊢W=1→∀i∈0..^WW⁡i=W⁡0
79 68 78 pm2.61d2 ⊢¬W=0∧W∈WordV∧WcyclShift1=W→∀i∈0..^WW⁡i=W⁡0
80 79 ex ⊢¬W=0→W∈WordV∧WcyclShift1=W→∀i∈0..^WW⁡i=W⁡0
81 7 80 pm2.61i ⊢W∈WordV∧WcyclShift1=W→∀i∈0..^WW⁡i=W⁡0