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

Metamath Proof Explorer

Theorem cshweqdifid

Description: If cyclically shifting a word by two positions results in the same word, cyclically shifting the word by the difference of these two positions results in the original word itself. (Contributed by AV, 21-Apr-2018) (Revised by AV, 7-Jun-2018) (Revised by AV, 1-Nov-2018)

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

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word 𝑉 )
2 1 ancli ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉 ) )
3 2 anim1i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) )
4 3 3impb ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) )
5 cshweqdif2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift 𝑀 ) → ( 𝑊 cyclShift ( 𝑀 − 𝑁 ) ) = 𝑊 ) )
6 4 5 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift 𝑀 ) → ( 𝑊 cyclShift ( 𝑀 − 𝑁 ) ) = 𝑊 ) )