# 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 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\wedge {M}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}{M}\to {W}\mathrm{cyclShift}\left({M}-{N}\right)={W}\right)$

### Proof

Step Hyp Ref Expression
1 id ${⊢}{W}\in \mathrm{Word}{V}\to {W}\in \mathrm{Word}{V}$
2 1 ancli ${⊢}{W}\in \mathrm{Word}{V}\to \left({W}\in \mathrm{Word}{V}\wedge {W}\in \mathrm{Word}{V}\right)$
3 2 anim1i ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({N}\in ℤ\wedge {M}\in ℤ\right)\right)\to \left(\left({W}\in \mathrm{Word}{V}\wedge {W}\in \mathrm{Word}{V}\right)\wedge \left({N}\in ℤ\wedge {M}\in ℤ\right)\right)$
4 3 3impb ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\wedge {M}\in ℤ\right)\to \left(\left({W}\in \mathrm{Word}{V}\wedge {W}\in \mathrm{Word}{V}\right)\wedge \left({N}\in ℤ\wedge {M}\in ℤ\right)\right)$
5 cshweqdif2 ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge {W}\in \mathrm{Word}{V}\right)\wedge \left({N}\in ℤ\wedge {M}\in ℤ\right)\right)\to \left({W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}{M}\to {W}\mathrm{cyclShift}\left({M}-{N}\right)={W}\right)$
6 4 5 syl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\wedge {M}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}{M}\to {W}\mathrm{cyclShift}\left({M}-{N}\right)={W}\right)$