Metamath Proof Explorer

Theorem 2cshwcom

Description: Cyclically shifting a word two times is commutative. (Contributed by AV, 21-Apr-2018) (Revised by AV, 5-Jun-2018) (Revised by Mario Carneiro/AV, 1-Nov-2018)

		Ref	Expression
	Assertion	2cshwcom	$⊢ (W \in Word V \land N \in ℤ \land M \in ℤ) \to (W cyclShift N) cyclShift M = (W cyclShift M) cyclShift N$

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ M \in ℤ \to M \in ℂ$
2		zcn	$⊢ N \in ℤ \to N \in ℂ$
3		addcom	$⊢ (M \in ℂ \land N \in ℂ) \to M + N = N + M$
4	1 2 3	syl2anr	$⊢ (N \in ℤ \land M \in ℤ) \to M + N = N + M$
5	4	3adant1	$⊢ (W \in Word V \land N \in ℤ \land M \in ℤ) \to M + N = N + M$
6	5	oveq2d	$⊢ (W \in Word V \land N \in ℤ \land M \in ℤ) \to W cyclShift (M + N) = W cyclShift (N + M)$
7		2cshw	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to (W cyclShift M) cyclShift N = W cyclShift (M + N)$
8	7	3com23	$⊢ (W \in Word V \land N \in ℤ \land M \in ℤ) \to (W cyclShift M) cyclShift N = W cyclShift (M + N)$
9		2cshw	$⊢ (W \in Word V \land N \in ℤ \land M \in ℤ) \to (W cyclShift N) cyclShift M = W cyclShift (N + M)$
10	6 8 9	3eqtr4rd	$⊢ (W \in Word V \land N \in ℤ \land M \in ℤ) \to (W cyclShift N) cyclShift M = (W cyclShift M) cyclShift N$