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 imbitrrid ⊢ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 𝑚 ∈ ( 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 𝑛 ) ) )