# Metamath Proof Explorer

## Theorem cshwshashlem1

Description: If cyclically shifting a word of length being a prime number not consisting of identical symbols by at least one position (and not by as many positions as the length of the word), the result will not be the word itself. (Contributed by AV, 19-May-2018) (Revised by AV, 8-Jun-2018) (Revised by AV, 10-Nov-2018)

Ref Expression
Hypothesis cshwshash.0 ( 𝜑 → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) )
Assertion cshwshashlem1 ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ∧ 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ 𝑊 )

### Proof

Step Hyp Ref Expression
1 cshwshash.0 ( 𝜑 → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) )
2 df-ne ( ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ↔ ¬ ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
3 2 rexbii ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ¬ ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
4 rexnal ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ¬ ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ¬ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
5 3 4 bitri ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ↔ ¬ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
6 simpll ( ( ( 𝜑𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → 𝜑 )
7 fzo0ss1 ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) )
8 fzossfz ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑊 ) )
9 7 8 sstri ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑊 ) )
10 9 sseli ( 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
11 10 ad2antlr ( ( ( 𝜑𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
12 simpr ( ( ( 𝜑𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝑊 cyclShift 𝐿 ) = 𝑊 )
13 simpll ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 )
14 simpr ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ♯ ‘ 𝑊 ) ∈ ℙ )
15 14 adantr ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℙ )
16 elfzelz ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℤ )
17 16 adantl ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝐿 ∈ ℤ )
18 cshwsidrepswmod0 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ∧ 𝐿 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) ) )
19 13 15 17 18 syl3anc ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) ) )
20 19 ex ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) ) ) )
21 20 3imp ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )
22 olc ( 𝐿 = ( ♯ ‘ 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ) )
23 22 a1d ( 𝐿 = ( ♯ ‘ 𝑊 ) → ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ) ) )
24 fzofzim ( ( 𝐿 ≠ ( ♯ ‘ 𝑊 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
25 zmodidfzoimp ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 𝐿 )
26 eqtr2 ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 𝐿 ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ) → 𝐿 = 0 )
27 26 a1d ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 𝐿 ∧ ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → 𝐿 = 0 ) )
28 27 ex ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 𝐿 → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → 𝐿 = 0 ) ) )
29 25 28 syl ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → 𝐿 = 0 ) ) )
30 24 29 syl ( ( 𝐿 ≠ ( ♯ ‘ 𝑊 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → 𝐿 = 0 ) ) )
31 30 expcom ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 𝐿 ≠ ( ♯ ‘ 𝑊 ) → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → 𝐿 = 0 ) ) ) )
32 31 com24 ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 → ( 𝐿 ≠ ( ♯ ‘ 𝑊 ) → 𝐿 = 0 ) ) ) )
33 32 impcom ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 → ( 𝐿 ≠ ( ♯ ‘ 𝑊 ) → 𝐿 = 0 ) ) )
34 33 3adant3 ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 → ( 𝐿 ≠ ( ♯ ‘ 𝑊 ) → 𝐿 = 0 ) ) )
35 34 impcom ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ( 𝐿 ≠ ( ♯ ‘ 𝑊 ) → 𝐿 = 0 ) )
36 35 impcom ( ( 𝐿 ≠ ( ♯ ‘ 𝑊 ) ∧ ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ) → 𝐿 = 0 )
37 36 orcd ( ( 𝐿 ≠ ( ♯ ‘ 𝑊 ) ∧ ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ) )
38 37 ex ( 𝐿 ≠ ( ♯ ‘ 𝑊 ) → ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ) ) )
39 23 38 pm2.61ine ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ) )
40 39 orcd ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ( ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ) ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )
41 df-3or ( ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) ↔ ( ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ) ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )
42 40 41 sylibr ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∧ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )
43 42 ex ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) ) )
44 3mix3 ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )
45 44 a1d ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) ) )
46 43 45 jaoi ( ( ( 𝐿 mod ( ♯ ‘ 𝑊 ) ) = 0 ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) ) )
47 21 46 mpcom ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )
48 1 47 syl3an1 ( ( 𝜑𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) )
49 3mix1 ( 𝐿 = 0 → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
50 49 a1d ( 𝐿 = 0 → ( ( 𝜑𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) ) )
51 3mix2 ( 𝐿 = ( ♯ ‘ 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
52 51 a1d ( 𝐿 = ( ♯ ‘ 𝑊 ) → ( ( 𝜑𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) ) )
53 repswsymballbi ( 𝑊 ∈ Word 𝑉 → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
54 53 adantr ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
55 1 54 syl ( 𝜑 → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
56 55 3ad2ant1 ( ( 𝜑𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
57 56 biimpa ( ( ( 𝜑𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ∧ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
58 57 3mix3d ( ( ( 𝜑𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) ∧ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
59 58 expcom ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) → ( ( 𝜑𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) ) )
60 50 52 59 3jaoi ( ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝜑𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) ) )
61 48 60 mpcom ( ( 𝜑𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
62 6 11 12 61 syl3anc ( ( ( 𝜑𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
63 elfzo1 ( 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝐿 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐿 < ( ♯ ‘ 𝑊 ) ) )
64 nnne0 ( 𝐿 ∈ ℕ → 𝐿 ≠ 0 )
65 df-ne ( 𝐿 ≠ 0 ↔ ¬ 𝐿 = 0 )
66 pm2.21 ( ¬ 𝐿 = 0 → ( 𝐿 = 0 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
67 65 66 sylbi ( 𝐿 ≠ 0 → ( 𝐿 = 0 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
68 64 67 syl ( 𝐿 ∈ ℕ → ( 𝐿 = 0 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
69 68 3ad2ant1 ( ( 𝐿 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐿 < ( ♯ ‘ 𝑊 ) ) → ( 𝐿 = 0 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
70 63 69 sylbi ( 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐿 = 0 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
71 70 ad2antlr ( ( ( 𝜑𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = 0 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
72 71 com12 ( 𝐿 = 0 → ( ( ( 𝜑𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
73 nnre ( 𝐿 ∈ ℕ → 𝐿 ∈ ℝ )
74 ltne ( ( 𝐿 ∈ ℝ ∧ 𝐿 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ≠ 𝐿 )
75 73 74 sylan ( ( 𝐿 ∈ ℕ ∧ 𝐿 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ≠ 𝐿 )
76 df-ne ( ( ♯ ‘ 𝑊 ) ≠ 𝐿 ↔ ¬ ( ♯ ‘ 𝑊 ) = 𝐿 )
77 eqcom ( 𝐿 = ( ♯ ‘ 𝑊 ) ↔ ( ♯ ‘ 𝑊 ) = 𝐿 )
78 pm2.21 ( ¬ ( ♯ ‘ 𝑊 ) = 𝐿 → ( ( ♯ ‘ 𝑊 ) = 𝐿 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
79 77 78 syl5bi ( ¬ ( ♯ ‘ 𝑊 ) = 𝐿 → ( 𝐿 = ( ♯ ‘ 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
80 76 79 sylbi ( ( ♯ ‘ 𝑊 ) ≠ 𝐿 → ( 𝐿 = ( ♯ ‘ 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
81 75 80 syl ( ( 𝐿 ∈ ℕ ∧ 𝐿 < ( ♯ ‘ 𝑊 ) ) → ( 𝐿 = ( ♯ ‘ 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
82 81 3adant2 ( ( 𝐿 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐿 < ( ♯ ‘ 𝑊 ) ) → ( 𝐿 = ( ♯ ‘ 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
83 63 82 sylbi ( 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐿 = ( ♯ ‘ 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
84 83 ad2antlr ( ( ( 𝜑𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( 𝐿 = ( ♯ ‘ 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
85 84 com12 ( 𝐿 = ( ♯ ‘ 𝑊 ) → ( ( ( 𝜑𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
86 ax-1 ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) → ( ( ( 𝜑𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
87 72 85 86 3jaoi ( ( 𝐿 = 0 ∨ 𝐿 = ( ♯ ‘ 𝑊 ) ∨ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) → ( ( ( 𝜑𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
88 62 87 mpcom ( ( ( 𝜑𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
89 88 pm2.24d ( ( ( 𝜑𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑊 cyclShift 𝐿 ) = 𝑊 ) → ( ¬ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) → ( 𝑊 cyclShift 𝐿 ) ≠ 𝑊 ) )
90 89 exp31 ( 𝜑 → ( 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( ¬ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) → ( 𝑊 cyclShift 𝐿 ) ≠ 𝑊 ) ) ) )
91 90 com34 ( 𝜑 → ( 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → ( ¬ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( 𝑊 cyclShift 𝐿 ) ≠ 𝑊 ) ) ) )
92 91 com23 ( 𝜑 → ( ¬ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) → ( 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( 𝑊 cyclShift 𝐿 ) ≠ 𝑊 ) ) ) )
93 5 92 syl5bi ( 𝜑 → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) → ( 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( 𝑊 cyclShift 𝐿 ) ≠ 𝑊 ) ) ) )
94 93 3imp ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ∧ 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( 𝑊 cyclShift 𝐿 ) ≠ 𝑊 ) )
95 94 com12 ( ( 𝑊 cyclShift 𝐿 ) = 𝑊 → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ∧ 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ 𝑊 ) )
96 ax-1 ( ( 𝑊 cyclShift 𝐿 ) ≠ 𝑊 → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ∧ 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ 𝑊 ) )
97 95 96 pm2.61ine ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ≠ ( 𝑊 ‘ 0 ) ∧ 𝐿 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝐿 ) ≠ 𝑊 )