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 \in Word V \land N \in ℤ \land M \in ℤ) \to (W cyclShift N = W cyclShift M \to W cyclShift (M - N) = W)$

Proof

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

Metamath Proof Explorer

Theorem cshweqdifid

Proof