Metamath Proof Explorer

Theorem cshweqdif2

Description: If cyclically shifting two words (of the same length) results in the same word, cyclically shifting one of the words by the difference of the numbers of shifts results in the other word. (Contributed by AV, 21-Apr-2018) (Revised by AV, 6-Jun-2018) (Revised by AV, 1-Nov-2018)

Ref Expression
Assertion cshweqdif2 ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) → ( 𝑈 cyclShift ( 𝑀 − 𝑁 ) ) = 𝑊 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) → 𝑈 ∈ Word 𝑉 )
2 1 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝑈 ∈ Word 𝑉 )
3 zsubcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
4 3 ancoms ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
5 4 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
6 simpr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
7 6 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
8 2 5 7 3jca ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑈 ∈ Word 𝑉 ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
9 8 adantr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑈 ∈ Word 𝑉 ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
10 3cshw ⊢ ( ( 𝑈 ∈ Word 𝑉 ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑈 cyclShift ( 𝑀 − 𝑁 ) ) = ( ( ( 𝑈 cyclShift 𝑀 ) cyclShift ( 𝑀 − 𝑁 ) ) cyclShift ( ( ♯ ‘ 𝑈 ) − 𝑀 ) ) )
11 9 10 syl ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑈 cyclShift ( 𝑀 − 𝑁 ) ) = ( ( ( 𝑈 cyclShift 𝑀 ) cyclShift ( 𝑀 − 𝑁 ) ) cyclShift ( ( ♯ ‘ 𝑈 ) − 𝑀 ) ) )
12 simpl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) )
13 12 ancomd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑈 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉 ) )
14 13 adantr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑈 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉 ) )
15 simpr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
16 15 ancomd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
17 16 adantr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
18 simpr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) )
19 18 eqcomd ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑈 cyclShift 𝑀 ) = ( 𝑊 cyclShift 𝑁 ) )
20 cshwleneq ⊢ ( ( ( 𝑈 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑈 cyclShift 𝑀 ) = ( 𝑊 cyclShift 𝑁 ) ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) )
21 14 17 19 20 syl3anc ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) )
22 21 oveq1d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ( ♯ ‘ 𝑈 ) − 𝑀 ) = ( ( ♯ ‘ 𝑊 ) − 𝑀 ) )
23 22 oveq2d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ( ( 𝑈 cyclShift 𝑀 ) cyclShift ( 𝑀 − 𝑁 ) ) cyclShift ( ( ♯ ‘ 𝑈 ) − 𝑀 ) ) = ( ( ( 𝑈 cyclShift 𝑀 ) cyclShift ( 𝑀 − 𝑁 ) ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) )
24 11 23 eqtrd ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑈 cyclShift ( 𝑀 − 𝑁 ) ) = ( ( ( 𝑈 cyclShift 𝑀 ) cyclShift ( 𝑀 − 𝑁 ) ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) )
25 19 oveq1d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ( 𝑈 cyclShift 𝑀 ) cyclShift ( 𝑀 − 𝑁 ) ) = ( ( 𝑊 cyclShift 𝑁 ) cyclShift ( 𝑀 − 𝑁 ) ) )
26 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) → 𝑊 ∈ Word 𝑉 )
27 26 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝑊 ∈ Word 𝑉 )
28 simpl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝑁 ∈ ℤ )
29 28 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
30 27 29 5 3jca ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ) )
31 30 adantr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ) )
32 2cshw ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) cyclShift ( 𝑀 − 𝑁 ) ) = ( 𝑊 cyclShift ( 𝑁 + ( 𝑀 − 𝑁 ) ) ) )
33 31 32 syl ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ( 𝑊 cyclShift 𝑁 ) cyclShift ( 𝑀 − 𝑁 ) ) = ( 𝑊 cyclShift ( 𝑁 + ( 𝑀 − 𝑁 ) ) ) )
34 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
35 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
36 34 35 anim12i ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) )
37 36 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) )
38 37 adantr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) )
39 pncan3 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝑁 + ( 𝑀 − 𝑁 ) ) = 𝑀 )
40 38 39 syl ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑁 + ( 𝑀 − 𝑁 ) ) = 𝑀 )
41 40 oveq2d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑊 cyclShift ( 𝑁 + ( 𝑀 − 𝑁 ) ) ) = ( 𝑊 cyclShift 𝑀 ) )
42 25 33 41 3eqtrd ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ( 𝑈 cyclShift 𝑀 ) cyclShift ( 𝑀 − 𝑁 ) ) = ( 𝑊 cyclShift 𝑀 ) )
43 42 oveq1d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ( ( 𝑈 cyclShift 𝑀 ) cyclShift ( 𝑀 − 𝑁 ) ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) = ( ( 𝑊 cyclShift 𝑀 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) )
44 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
45 44 nn0zd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
46 45 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
47 zsubcl ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ∈ ℤ )
48 46 6 47 syl2an ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ∈ ℤ )
49 27 7 48 3jca ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ∈ ℤ ) )
50 49 adantr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ∈ ℤ ) )
51 2cshw ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑀 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) = ( 𝑊 cyclShift ( 𝑀 + ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) ) )
52 50 51 syl ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( ( 𝑊 cyclShift 𝑀 ) cyclShift ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) = ( 𝑊 cyclShift ( 𝑀 + ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) ) )
53 24 43 52 3eqtrd ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑈 cyclShift ( 𝑀 − 𝑁 ) ) = ( 𝑊 cyclShift ( 𝑀 + ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) ) )
54 44 nn0cnd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
55 54 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
56 35 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℂ )
57 55 56 anim12i ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℂ ∧ 𝑀 ∈ ℂ ) )
58 57 ancomd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑀 ∈ ℂ ∧ ( ♯ ‘ 𝑊 ) ∈ ℂ ) )
59 58 adantr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑀 ∈ ℂ ∧ ( ♯ ‘ 𝑊 ) ∈ ℂ ) )
60 pncan3 ⊢ ( ( 𝑀 ∈ ℂ ∧ ( ♯ ‘ 𝑊 ) ∈ ℂ ) → ( 𝑀 + ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) = ( ♯ ‘ 𝑊 ) )
61 59 60 syl ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑀 + ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) = ( ♯ ‘ 𝑊 ) )
62 61 oveq2d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑊 cyclShift ( 𝑀 + ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) ) = ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) )
63 cshwn ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 )
64 27 63 syl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 )
65 64 adantr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑊 cyclShift ( ♯ ‘ 𝑊 ) ) = 𝑊 )
66 53 62 65 3eqtrd ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) ) → ( 𝑈 cyclShift ( 𝑀 − 𝑁 ) ) = 𝑊 )
67 66 ex ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝑊 cyclShift 𝑁 ) = ( 𝑈 cyclShift 𝑀 ) → ( 𝑈 cyclShift ( 𝑀 − 𝑁 ) ) = 𝑊 ) )