Metamath Proof Explorer

Theorem 2cshwcshw

Description: If a word is a cyclically shifted word, and a second word is the result of cyclically shifting the same word, then the second word is the result of cyclically shifting the first word. (Contributed by AV, 11-May-2018) (Revised by AV, 12-Jun-2018) (Proof shortened by AV, 3-Nov-2018)

Ref Expression
Assertion 2cshwcshw ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ∧ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 difelfznle ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾𝑚 ) → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) )
2 1 3exp ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ¬ 𝐾𝑚 → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) ) ) )
3 2 ad2antrr ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ¬ 𝐾𝑚 → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) ) ) )
4 3 imp ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( ¬ 𝐾𝑚 → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) ) )
5 4 adantr ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ( ¬ 𝐾𝑚 → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) ) )
6 5 com12 ( ¬ 𝐾𝑚 → ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) ) )
7 6 adantl ( ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) → ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) ) )
8 7 imp ( ( ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ∧ ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) ) → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) )
9 simprl ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → 𝑌 ∈ Word 𝑉 )
10 9 ad2antrr ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → 𝑌 ∈ Word 𝑉 )
11 elfzelz ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℤ )
12 11 adantr ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → 𝐾 ∈ ℤ )
13 12 ad2antrr ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℤ )
14 elfz2 ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 0 ≤ 𝐾𝐾𝑁 ) ) )
15 zaddcl ( ( 𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑚 + 𝑁 ) ∈ ℤ )
16 15 adantrr ( ( 𝑚 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑚 + 𝑁 ) ∈ ℤ )
17 simprr ( ( 𝑚 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → 𝐾 ∈ ℤ )
18 16 17 zsubcld ( ( 𝑚 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ℤ )
19 18 ex ( 𝑚 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ℤ ) )
20 elfzelz ( 𝑚 ∈ ( 0 ... 𝑁 ) → 𝑚 ∈ ℤ )
21 19 20 syl11 ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ℤ ) )
22 21 3adant1 ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ℤ ) )
23 22 adantr ( ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 0 ≤ 𝐾𝐾𝑁 ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ℤ ) )
24 14 23 sylbi ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ℤ ) )
25 24 ad2antrr ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ℤ ) )
26 25 imp ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ℤ )
27 2cshw ( ( 𝑌 ∈ Word 𝑉𝐾 ∈ ℤ ∧ ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ℤ ) → ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) = ( 𝑌 cyclShift ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ) )
28 10 13 26 27 syl3anc ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) = ( 𝑌 cyclShift ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ) )
29 17 18 zaddcld ( ( 𝑚 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ∈ ℤ )
30 29 ex ( 𝑚 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ∈ ℤ ) )
31 30 20 syl11 ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ∈ ℤ ) )
32 31 3adant1 ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ∈ ℤ ) )
33 32 adantr ( ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 0 ≤ 𝐾𝐾𝑁 ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ∈ ℤ ) )
34 14 33 sylbi ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ∈ ℤ ) )
35 34 ad2antrr ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ∈ ℤ ) )
36 35 imp ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ∈ ℤ )
37 cshwsublen ( ( 𝑌 ∈ Word 𝑉 ∧ ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ∈ ℤ ) → ( 𝑌 cyclShift ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ) = ( 𝑌 cyclShift ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − ( ♯ ‘ 𝑌 ) ) ) )
38 10 36 37 syl2anc ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑌 cyclShift ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ) = ( 𝑌 cyclShift ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − ( ♯ ‘ 𝑌 ) ) ) )
39 28 38 eqtrd ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) = ( 𝑌 cyclShift ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − ( ♯ ‘ 𝑌 ) ) ) )
40 elfz2nn0 ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁 ) )
41 nn0cn ( 𝑚 ∈ ℕ0𝑚 ∈ ℂ )
42 nn0cn ( 𝐾 ∈ ℕ0𝐾 ∈ ℂ )
43 nn0cn ( 𝑁 ∈ ℕ0𝑁 ∈ ℂ )
44 42 43 anim12i ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
45 simprl ( ( 𝑚 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) → 𝐾 ∈ ℂ )
46 addcl ( ( 𝑚 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑚 + 𝑁 ) ∈ ℂ )
47 46 adantrl ( ( 𝑚 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) → ( 𝑚 + 𝑁 ) ∈ ℂ )
48 45 47 pncan3d ( ( 𝑚 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) → ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) = ( 𝑚 + 𝑁 ) )
49 48 oveq1d ( ( 𝑚 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) = ( ( 𝑚 + 𝑁 ) − 𝑁 ) )
50 pncan ( ( 𝑚 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑚 + 𝑁 ) − 𝑁 ) = 𝑚 )
51 50 adantrl ( ( 𝑚 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) → ( ( 𝑚 + 𝑁 ) − 𝑁 ) = 𝑚 )
52 49 51 eqtrd ( ( 𝑚 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) = 𝑚 )
53 41 44 52 syl2an ( ( 𝑚 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) = 𝑚 )
54 53 ex ( 𝑚 ∈ ℕ0 → ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) = 𝑚 ) )
55 elfznn0 ( 𝑚 ∈ ( 0 ... 𝑁 ) → 𝑚 ∈ ℕ0 )
56 54 55 syl11 ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) = 𝑚 ) )
57 56 3adant3 ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) = 𝑚 ) )
58 40 57 sylbi ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) = 𝑚 ) )
59 58 adantr ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) = 𝑚 ) )
60 oveq2 ( ( ♯ ‘ 𝑌 ) = 𝑁 → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − ( ♯ ‘ 𝑌 ) ) = ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) )
61 60 eqeq1d ( ( ♯ ‘ 𝑌 ) = 𝑁 → ( ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − ( ♯ ‘ 𝑌 ) ) = 𝑚 ↔ ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) = 𝑚 ) )
62 61 imbi2d ( ( ♯ ‘ 𝑌 ) = 𝑁 → ( ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − ( ♯ ‘ 𝑌 ) ) = 𝑚 ) ↔ ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) = 𝑚 ) ) )
63 62 adantl ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → ( ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − ( ♯ ‘ 𝑌 ) ) = 𝑚 ) ↔ ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) = 𝑚 ) ) )
64 63 adantl ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ( ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − ( ♯ ‘ 𝑌 ) ) = 𝑚 ) ↔ ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − 𝑁 ) = 𝑚 ) ) )
65 59 64 mpbird ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − ( ♯ ‘ 𝑌 ) ) = 𝑚 ) )
66 65 adantr ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − ( ♯ ‘ 𝑌 ) ) = 𝑚 ) )
67 66 imp ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − ( ♯ ‘ 𝑌 ) ) = 𝑚 )
68 67 oveq2d ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑌 cyclShift ( ( 𝐾 + ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) − ( ♯ ‘ 𝑌 ) ) ) = ( 𝑌 cyclShift 𝑚 ) )
69 39 68 eqtr2d ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑌 cyclShift 𝑚 ) = ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) )
70 69 adantr ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( 𝑌 cyclShift 𝑚 ) = ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) )
71 oveq1 ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝑋 cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) = ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) )
72 71 adantl ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( 𝑋 cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) = ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) )
73 70 72 eqtr4d ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( 𝑌 cyclShift 𝑚 ) = ( 𝑋 cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) )
74 73 exp41 ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ( ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝑌 cyclShift 𝑚 ) = ( 𝑋 cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ) ) ) )
75 74 com24 ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) → ( 𝑌 cyclShift 𝑚 ) = ( 𝑋 cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ) ) ) )
76 75 imp41 ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) → ( 𝑌 cyclShift 𝑚 ) = ( 𝑋 cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) )
77 76 eqeq2d ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) → ( 𝑍 = ( 𝑌 cyclShift 𝑚 ) ↔ 𝑍 = ( 𝑋 cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ) )
78 77 biimpd ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ) → ( 𝑍 = ( 𝑌 cyclShift 𝑚 ) → 𝑍 = ( 𝑋 cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ) )
79 78 impancom ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ( ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) → 𝑍 = ( 𝑋 cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ) )
80 79 impcom ( ( ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ∧ ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) ) → 𝑍 = ( 𝑋 cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) )
81 oveq2 ( 𝑛 = ( ( 𝑚 + 𝑁 ) − 𝐾 ) → ( 𝑋 cyclShift 𝑛 ) = ( 𝑋 cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) )
82 81 rspceeqv ( ( ( ( 𝑚 + 𝑁 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) ∧ 𝑍 = ( 𝑋 cyclShift ( ( 𝑚 + 𝑁 ) − 𝐾 ) ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) )
83 8 80 82 syl2anc ( ( ( ¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚 ) ∧ ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) )
84 83 exp31 ( ¬ 𝑚 = 0 → ( ¬ 𝐾𝑚 → ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) )
85 oveq2 ( 𝑚 = 0 → ( 𝑌 cyclShift 𝑚 ) = ( 𝑌 cyclShift 0 ) )
86 85 eqeq2d ( 𝑚 = 0 → ( 𝑍 = ( 𝑌 cyclShift 𝑚 ) ↔ 𝑍 = ( 𝑌 cyclShift 0 ) ) )
87 cshw0 ( 𝑌 ∈ Word 𝑉 → ( 𝑌 cyclShift 0 ) = 𝑌 )
88 87 adantr ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → ( 𝑌 cyclShift 0 ) = 𝑌 )
89 88 eqeq2d ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → ( 𝑍 = ( 𝑌 cyclShift 0 ) ↔ 𝑍 = 𝑌 ) )
90 fznn0sub2 ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) )
91 90 adantl ( ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) )
92 oveq1 ( ( ♯ ‘ 𝑌 ) = 𝑁 → ( ( ♯ ‘ 𝑌 ) − 𝐾 ) = ( 𝑁𝐾 ) )
93 92 eleq1d ( ( ♯ ‘ 𝑌 ) = 𝑁 → ( ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) ↔ ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) ) )
94 93 ad2antlr ( ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) ↔ ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) ) )
95 91 94 mpbird ( ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) )
96 95 adantr ( ( ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) )
97 oveq1 ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝑋 cyclShift ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ) = ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ) )
98 simpl ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → 𝑌 ∈ Word 𝑉 )
99 2cshwid ( ( 𝑌 ∈ Word 𝑉𝐾 ∈ ℤ ) → ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ) = 𝑌 )
100 98 11 99 syl2an ( ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ) = 𝑌 )
101 97 100 sylan9eqr ( ( ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( 𝑋 cyclShift ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ) = 𝑌 )
102 101 eqcomd ( ( ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → 𝑌 = ( 𝑋 cyclShift ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ) )
103 oveq2 ( 𝑛 = ( ( ♯ ‘ 𝑌 ) − 𝐾 ) → ( 𝑋 cyclShift 𝑛 ) = ( 𝑋 cyclShift ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ) )
104 103 rspceeqv ( ( ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) ∧ 𝑌 = ( 𝑋 cyclShift ( ( ♯ ‘ 𝑌 ) − 𝐾 ) ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) )
105 96 102 104 syl2anc ( ( ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) )
106 105 adantr ( ( ( ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑍 = 𝑌 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) )
107 eqeq1 ( 𝑍 = 𝑌 → ( 𝑍 = ( 𝑋 cyclShift 𝑛 ) ↔ 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) )
108 107 rexbidv ( 𝑍 = 𝑌 → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) )
109 108 adantl ( ( ( ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑍 = 𝑌 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) )
110 106 109 mpbird ( ( ( ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑍 = 𝑌 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) )
111 110 exp41 ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝑍 = 𝑌 → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) ) )
112 111 com24 ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → ( 𝑍 = 𝑌 → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) ) )
113 89 112 sylbid ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → ( 𝑍 = ( 𝑌 cyclShift 0 ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) ) )
114 113 com24 ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝑍 = ( 𝑌 cyclShift 0 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) ) )
115 114 impcom ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝑍 = ( 𝑌 cyclShift 0 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) )
116 115 com13 ( 𝑍 = ( 𝑌 cyclShift 0 ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) )
117 116 a1d ( 𝑍 = ( 𝑌 cyclShift 0 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) ) )
118 86 117 syl6bi ( 𝑚 = 0 → ( 𝑍 = ( 𝑌 cyclShift 𝑚 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) ) ) )
119 118 com24 ( 𝑚 = 0 → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝑍 = ( 𝑌 cyclShift 𝑚 ) → ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) ) ) )
120 119 com15 ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝑍 = ( 𝑌 cyclShift 𝑚 ) → ( 𝑚 = 0 → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) ) ) )
121 120 imp41 ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ( 𝑚 = 0 → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) )
122 121 com12 ( 𝑚 = 0 → ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) )
123 difelfzle ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝐾𝑚 ) → ( 𝑚𝐾 ) ∈ ( 0 ... 𝑁 ) )
124 123 3exp ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝐾𝑚 → ( 𝑚𝐾 ) ∈ ( 0 ... 𝑁 ) ) ) )
125 124 ad2antrr ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝐾𝑚 → ( 𝑚𝐾 ) ∈ ( 0 ... 𝑁 ) ) ) )
126 125 imp ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝐾𝑚 → ( 𝑚𝐾 ) ∈ ( 0 ... 𝑁 ) ) )
127 126 adantr ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ( 𝐾𝑚 → ( 𝑚𝐾 ) ∈ ( 0 ... 𝑁 ) ) )
128 127 impcom ( ( 𝐾𝑚 ∧ ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) ) → ( 𝑚𝐾 ) ∈ ( 0 ... 𝑁 ) )
129 9 ad2antrr ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → 𝑌 ∈ Word 𝑉 )
130 12 ad2antrr ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℤ )
131 zsubcl ( ( 𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚𝐾 ) ∈ ℤ )
132 131 ex ( 𝑚 ∈ ℤ → ( 𝐾 ∈ ℤ → ( 𝑚𝐾 ) ∈ ℤ ) )
133 20 11 132 syl2imc ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝑚𝐾 ) ∈ ℤ ) )
134 133 ad2antrr ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝑚𝐾 ) ∈ ℤ ) )
135 134 imp ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑚𝐾 ) ∈ ℤ )
136 2cshw ( ( 𝑌 ∈ Word 𝑉𝐾 ∈ ℤ ∧ ( 𝑚𝐾 ) ∈ ℤ ) → ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( 𝑚𝐾 ) ) = ( 𝑌 cyclShift ( 𝐾 + ( 𝑚𝐾 ) ) ) )
137 129 130 135 136 syl3anc ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( 𝑚𝐾 ) ) = ( 𝑌 cyclShift ( 𝐾 + ( 𝑚𝐾 ) ) ) )
138 zcn ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
139 20 zcnd ( 𝑚 ∈ ( 0 ... 𝑁 ) → 𝑚 ∈ ℂ )
140 pncan3 ( ( 𝐾 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 𝐾 + ( 𝑚𝐾 ) ) = 𝑚 )
141 138 139 140 syl2anr ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 + ( 𝑚𝐾 ) ) = 𝑚 )
142 141 ex ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝐾 ∈ ℤ → ( 𝐾 + ( 𝑚𝐾 ) ) = 𝑚 ) )
143 11 142 syl5com ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + ( 𝑚𝐾 ) ) = 𝑚 ) )
144 143 ad2antrr ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + ( 𝑚𝐾 ) ) = 𝑚 ) )
145 144 imp ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝐾 + ( 𝑚𝐾 ) ) = 𝑚 )
146 145 oveq2d ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑌 cyclShift ( 𝐾 + ( 𝑚𝐾 ) ) ) = ( 𝑌 cyclShift 𝑚 ) )
147 137 146 eqtr2d ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑌 cyclShift 𝑚 ) = ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( 𝑚𝐾 ) ) )
148 147 adantr ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( 𝑌 cyclShift 𝑚 ) = ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( 𝑚𝐾 ) ) )
149 oveq1 ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝑋 cyclShift ( 𝑚𝐾 ) ) = ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( 𝑚𝐾 ) ) )
150 149 eqeq2d ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( ( 𝑌 cyclShift 𝑚 ) = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) ↔ ( 𝑌 cyclShift 𝑚 ) = ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( 𝑚𝐾 ) ) ) )
151 150 adantl ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( ( 𝑌 cyclShift 𝑚 ) = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) ↔ ( 𝑌 cyclShift 𝑚 ) = ( ( 𝑌 cyclShift 𝐾 ) cyclShift ( 𝑚𝐾 ) ) ) )
152 148 151 mpbird ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( 𝑌 cyclShift 𝑚 ) = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) )
153 152 eqeq2d ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( 𝑍 = ( 𝑌 cyclShift 𝑚 ) ↔ 𝑍 = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) ) )
154 153 biimpd ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝐾𝑚 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( 𝑍 = ( 𝑌 cyclShift 𝑚 ) → 𝑍 = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) ) )
155 154 exp41 ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ( 𝐾𝑚 → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝑍 = ( 𝑌 cyclShift 𝑚 ) → 𝑍 = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) ) ) ) ) )
156 155 com24 ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝐾𝑚 → ( 𝑍 = ( 𝑌 cyclShift 𝑚 ) → 𝑍 = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) ) ) ) ) )
157 156 imp31 ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝐾𝑚 → ( 𝑍 = ( 𝑌 cyclShift 𝑚 ) → 𝑍 = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) ) ) )
158 157 com23 ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑍 = ( 𝑌 cyclShift 𝑚 ) → ( 𝐾𝑚𝑍 = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) ) ) )
159 158 imp ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ( 𝐾𝑚𝑍 = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) ) )
160 159 impcom ( ( 𝐾𝑚 ∧ ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) ) → 𝑍 = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) )
161 oveq2 ( 𝑛 = ( 𝑚𝐾 ) → ( 𝑋 cyclShift 𝑛 ) = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) )
162 161 rspceeqv ( ( ( 𝑚𝐾 ) ∈ ( 0 ... 𝑁 ) ∧ 𝑍 = ( 𝑋 cyclShift ( 𝑚𝐾 ) ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) )
163 128 160 162 syl2anc ( ( 𝐾𝑚 ∧ ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) )
164 163 ex ( 𝐾𝑚 → ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) )
165 84 122 164 pm2.61ii ( ( ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) )
166 165 rexlimdva2 ( ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ) → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑌 cyclShift 𝑚 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) )
167 166 ex ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑌 cyclShift 𝑚 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) )
168 167 com23 ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) ) → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑌 cyclShift 𝑚 ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) )
169 168 ex ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑌 cyclShift 𝑚 ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) ) )
170 169 com24 ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑋 = ( 𝑌 cyclShift 𝐾 ) → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑌 cyclShift 𝑚 ) → ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) ) ) )
171 170 3imp ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ∧ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) )
172 171 com12 ( ( 𝑌 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑌 ) = 𝑁 ) → ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑌 cyclShift 𝐾 ) ∧ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑌 cyclShift 𝑚 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑋 cyclShift 𝑛 ) ) )