Metamath Proof Explorer


Theorem cshwcshid

Description: A cyclically shifted word can be reconstructed by cyclically shifting it again. Lemma for erclwwlksym and erclwwlknsym . (Contributed by AV, 8-Apr-2018) (Revised by AV, 11-Jun-2018) (Proof shortened by AV, 3-Nov-2018)

Ref Expression
Hypotheses cshwcshid.1 ( 𝜑𝑦 ∈ Word 𝑉 )
cshwcshid.2 ( 𝜑 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
Assertion cshwcshid ( 𝜑 → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 cshwcshid.1 ( 𝜑𝑦 ∈ Word 𝑉 )
2 cshwcshid.2 ( 𝜑 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
3 fznn0sub2 ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) )
4 oveq2 ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 0 ... ( ♯ ‘ 𝑥 ) ) = ( 0 ... ( ♯ ‘ 𝑦 ) ) )
5 4 eleq2d ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ↔ ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) )
6 3 5 syl5ibr ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
7 6 2 syl11 ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( 𝜑 → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
8 7 adantr ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ( 𝜑 → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
9 8 impcom ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) )
10 simpl ( ( 𝑦 ∈ Word 𝑉𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → 𝑦 ∈ Word 𝑉 )
11 elfzelz ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → 𝑚 ∈ ℤ )
12 11 adantl ( ( 𝑦 ∈ Word 𝑉𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → 𝑚 ∈ ℤ )
13 elfz2nn0 ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ↔ ( 𝑚 ∈ ℕ0 ∧ ( ♯ ‘ 𝑦 ) ∈ ℕ0𝑚 ≤ ( ♯ ‘ 𝑦 ) ) )
14 nn0z ( ( ♯ ‘ 𝑦 ) ∈ ℕ0 → ( ♯ ‘ 𝑦 ) ∈ ℤ )
15 nn0z ( 𝑚 ∈ ℕ0𝑚 ∈ ℤ )
16 zsubcl ( ( ( ♯ ‘ 𝑦 ) ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ )
17 14 15 16 syl2anr ( ( 𝑚 ∈ ℕ0 ∧ ( ♯ ‘ 𝑦 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ )
18 17 3adant3 ( ( 𝑚 ∈ ℕ0 ∧ ( ♯ ‘ 𝑦 ) ∈ ℕ0𝑚 ≤ ( ♯ ‘ 𝑦 ) ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ )
19 13 18 sylbi ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ )
20 19 adantl ( ( 𝑦 ∈ Word 𝑉𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ )
21 10 12 20 3jca ( ( 𝑦 ∈ Word 𝑉𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( 𝑦 ∈ Word 𝑉𝑚 ∈ ℤ ∧ ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ ) )
22 1 21 sylan ( ( 𝜑𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( 𝑦 ∈ Word 𝑉𝑚 ∈ ℤ ∧ ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ ) )
23 2cshw ( ( 𝑦 ∈ Word 𝑉𝑚 ∈ ℤ ∧ ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ ) → ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) = ( 𝑦 cyclShift ( 𝑚 + ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) )
24 22 23 syl ( ( 𝜑𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) = ( 𝑦 cyclShift ( 𝑚 + ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) )
25 nn0cn ( 𝑚 ∈ ℕ0𝑚 ∈ ℂ )
26 nn0cn ( ( ♯ ‘ 𝑦 ) ∈ ℕ0 → ( ♯ ‘ 𝑦 ) ∈ ℂ )
27 25 26 anim12i ( ( 𝑚 ∈ ℕ0 ∧ ( ♯ ‘ 𝑦 ) ∈ ℕ0 ) → ( 𝑚 ∈ ℂ ∧ ( ♯ ‘ 𝑦 ) ∈ ℂ ) )
28 27 3adant3 ( ( 𝑚 ∈ ℕ0 ∧ ( ♯ ‘ 𝑦 ) ∈ ℕ0𝑚 ≤ ( ♯ ‘ 𝑦 ) ) → ( 𝑚 ∈ ℂ ∧ ( ♯ ‘ 𝑦 ) ∈ ℂ ) )
29 13 28 sylbi ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( 𝑚 ∈ ℂ ∧ ( ♯ ‘ 𝑦 ) ∈ ℂ ) )
30 pncan3 ( ( 𝑚 ∈ ℂ ∧ ( ♯ ‘ 𝑦 ) ∈ ℂ ) → ( 𝑚 + ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) = ( ♯ ‘ 𝑦 ) )
31 29 30 syl ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( 𝑚 + ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) = ( ♯ ‘ 𝑦 ) )
32 31 adantl ( ( 𝜑𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( 𝑚 + ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) = ( ♯ ‘ 𝑦 ) )
33 32 oveq2d ( ( 𝜑𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( 𝑦 cyclShift ( 𝑚 + ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) = ( 𝑦 cyclShift ( ♯ ‘ 𝑦 ) ) )
34 cshwn ( 𝑦 ∈ Word 𝑉 → ( 𝑦 cyclShift ( ♯ ‘ 𝑦 ) ) = 𝑦 )
35 1 34 syl ( 𝜑 → ( 𝑦 cyclShift ( ♯ ‘ 𝑦 ) ) = 𝑦 )
36 35 adantr ( ( 𝜑𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( 𝑦 cyclShift ( ♯ ‘ 𝑦 ) ) = 𝑦 )
37 24 33 36 3eqtrrd ( ( 𝜑𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → 𝑦 = ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) )
38 37 adantrr ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ) → 𝑦 = ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) )
39 oveq1 ( 𝑥 = ( 𝑦 cyclShift 𝑚 ) → ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) = ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) )
40 39 eqeq2d ( 𝑥 = ( 𝑦 cyclShift 𝑚 ) → ( 𝑦 = ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ↔ 𝑦 = ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) )
41 40 adantl ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ( 𝑦 = ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ↔ 𝑦 = ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) )
42 41 adantl ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ) → ( 𝑦 = ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ↔ 𝑦 = ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) )
43 38 42 mpbird ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ) → 𝑦 = ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) )
44 oveq2 ( 𝑛 = ( ( ♯ ‘ 𝑦 ) − 𝑚 ) → ( 𝑥 cyclShift 𝑛 ) = ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) )
45 44 rspceeqv ( ( ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) )
46 9 43 45 syl2anc ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) )
47 46 ex ( 𝜑 → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) )