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 e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( ( W cyclShift N ) = ( W cyclShift M ) -> ( W cyclShift ( M - N ) ) = W ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( W e. Word V -> W e. Word V )
2 1 ancli 
 |-  ( W e. Word V -> ( W e. Word V /\ W e. Word V ) )
3 2 anim1i 
 |-  ( ( W e. Word V /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( ( W e. Word V /\ W e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) )
4 3 3impb 
 |-  ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( ( W e. Word V /\ W e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) )
5 cshweqdif2 
 |-  ( ( ( W e. Word V /\ W e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( ( W cyclShift N ) = ( W cyclShift M ) -> ( W cyclShift ( M - N ) ) = W ) )
6 4 5 syl 
 |-  ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( ( W cyclShift N ) = ( W cyclShift M ) -> ( W cyclShift ( M - N ) ) = W ) )