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 𝐿 ) ≠ 𝑊 )