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 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift N = W cyclShift M → W cyclShift M − N = W

Proof

Step Hyp Ref Expression
1 id ⊢ W ∈ Word V → W ∈ Word V
2 1 ancli ⊢ W ∈ Word V → W ∈ Word V ∧ W ∈ Word V
3 2 anim1i ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W ∈ Word V ∧ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ
4 3 3impb ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W ∈ Word V ∧ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ
5 cshweqdif2 ⊢ W ∈ Word V ∧ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift N = W cyclShift M → W cyclShift M − N = W
6 4 5 syl ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ M ∈ ℤ → W cyclShift N = W cyclShift M → W cyclShift M − N = W