Metamath Proof Explorer

Theorem clwwisshclwwslem

Description: Lemma for clwwisshclwws . (Contributed by AV, 24-Mar-2018) (Revised by AV, 28-Apr-2021)

Ref Expression
Assertion clwwisshclwwslem ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) − 1 ) ) { ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) , ( ( 𝑊 cyclShift 𝑁 ) ‘ ( 𝑗 + 1 ) ) } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢ ( 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℤ )
2 cshwlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
3 1 2 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
4 3 oveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
5 4 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
6 5 eleq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) − 1 ) ) ↔ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) )
7 6 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ( 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) − 1 ) ) ↔ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) )
8 simpll ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑊 ∈ Word 𝑉 )
9 1 ad2antlr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑁 ∈ ℤ )
10 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
11 nn0z ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
12 peano2zm ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ )
13 11 12 syl ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ )
14 nn0re ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
15 14 lem1d ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) )
16 eluz2 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ↔ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) ) )
17 13 11 15 16 syl3anbrc ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
18 10 17 syl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
19 18 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
20 fzoss2 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
21 19 20 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
22 21 sselda ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
23 cshwidxmod ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) = ( 𝑊 ‘ ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
24 8 9 22 23 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) = ( 𝑊 ‘ ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
25 elfzo1 ⊢ ( 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) )
26 25 simp2bi ⊢ ( 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
27 26 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
28 elfzom1p1elfzo ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
29 27 28 sylan ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
30 cshwidxmod ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( 𝑗 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( 𝑗 + 1 ) ) = ( 𝑊 ‘ ( ( ( 𝑗 + 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
31 8 9 29 30 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( 𝑗 + 1 ) ) = ( 𝑊 ‘ ( ( ( 𝑗 + 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
32 24 31 preq12d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → { ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) , ( ( 𝑊 cyclShift 𝑁 ) ‘ ( 𝑗 + 1 ) ) } = { ( 𝑊 ‘ ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) , ( 𝑊 ‘ ( ( ( 𝑗 + 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) } )
33 32 adantlr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → { ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) , ( ( 𝑊 cyclShift 𝑁 ) ‘ ( 𝑗 + 1 ) ) } = { ( 𝑊 ‘ ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) , ( 𝑊 ‘ ( ( ( 𝑗 + 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) } )
34 2z ⊢ 2 ∈ ℤ
35 34 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → 2 ∈ ℤ )
36 nnz ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℤ )
37 36 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
38 nnnn0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
39 38 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
40 nnne0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ≠ 0 )
41 40 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ≠ 0 )
42 1red ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → 1 ∈ ℝ )
43 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
44 43 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℝ )
45 nnre ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℝ )
46 45 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℝ )
47 nnge1 ⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
48 47 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → 1 ≤ 𝑁 )
49 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → 𝑁 < ( ♯ ‘ 𝑊 ) )
50 42 44 46 48 49 lelttrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → 1 < ( ♯ ‘ 𝑊 ) )
51 42 50 gtned ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ≠ 1 )
52 nn0n0n1ge2 ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ∧ ( ♯ ‘ 𝑊 ) ≠ 1 ) → 2 ≤ ( ♯ ‘ 𝑊 ) )
53 39 41 51 52 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → 2 ≤ ( ♯ ‘ 𝑊 ) )
54 eluz2 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) )
55 35 37 53 54 syl3anbrc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) )
56 25 55 sylbi ⊢ ( 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) )
57 56 ad3antlr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) )
58 elfzoelz ⊢ ( 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) → 𝑗 ∈ ℤ )
59 58 adantl ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑗 ∈ ℤ )
60 1 ad3antlr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑁 ∈ ℤ )
61 simplrl ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 )
62 lsw ⊢ ( 𝑊 ∈ Word 𝑉 → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
63 62 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
64 63 preq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } = { ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( 𝑊 ‘ 0 ) } )
65 64 eleq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ↔ { ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
66 65 biimpcd ⊢ ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → { ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
67 66 adantl ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → { ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) )
68 67 impcom ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → { ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 )
69 68 adantr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → { ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 )
70 clwwisshclwwslemlem ⊢ ( ( ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → { ( 𝑊 ‘ ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) , ( 𝑊 ‘ ( ( ( 𝑗 + 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) } ∈ 𝐸 )
71 57 59 60 61 69 70 syl311anc ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → { ( 𝑊 ‘ ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) , ( 𝑊 ‘ ( ( ( 𝑗 + 1 ) + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) } ∈ 𝐸 )
72 33 71 eqeltrd ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → { ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) , ( ( 𝑊 cyclShift 𝑁 ) ‘ ( 𝑗 + 1 ) ) } ∈ 𝐸 )
73 72 ex ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ( 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) → { ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) , ( ( 𝑊 cyclShift 𝑁 ) ‘ ( 𝑗 + 1 ) ) } ∈ 𝐸 ) )
74 7 73 sylbid ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ( 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) − 1 ) ) → { ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) , ( ( 𝑊 cyclShift 𝑁 ) ‘ ( 𝑗 + 1 ) ) } ∈ 𝐸 ) )
75 74 ralrimiv ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) → ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) − 1 ) ) { ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) , ( ( 𝑊 cyclShift 𝑁 ) ‘ ( 𝑗 + 1 ) ) } ∈ 𝐸 )
76 75 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) → ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) − 1 ) ) { ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) , ( ( 𝑊 cyclShift 𝑁 ) ‘ ( 𝑗 + 1 ) ) } ∈ 𝐸 ) )