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

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 ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )

Proof

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