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 ( 𝑀 − 𝑁 ) ) = 𝑊 ) )