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 ) ) } ∈ 𝐸 ) )