This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( 𝑚 = 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 𝑛 ) ) )