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 WWordVNMWcyclShiftN=WcyclShiftMWcyclShiftMN=W

Proof

Step Hyp Ref Expression
1 id WWordVWWordV
2 1 ancli WWordVWWordVWWordV
3 2 anim1i WWordVNMWWordVWWordVNM
4 3 3impb WWordVNMWWordVWWordVNM
5 cshweqdif2 WWordVWWordVNMWcyclShiftN=WcyclShiftMWcyclShiftMN=W
6 4 5 syl WWordVNMWcyclShiftN=WcyclShiftMWcyclShiftMN=W