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

Proof

Step	Hyp	Ref	Expression
1		zcn	|- ( M e. ZZ -> M e. CC )
2		zcn	|- ( N e. ZZ -> N e. CC )
3		addcom	|- ( ( M e. CC /\ N e. CC ) -> ( M + N ) = ( N + M ) )
4	1 2 3	syl2anr	|- ( ( N e. ZZ /\ M e. ZZ ) -> ( M + N ) = ( N + M ) )
5	4	3adant1	|- ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( M + N ) = ( N + M ) )
6	5	oveq2d	|- ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( W cyclShift ( M + N ) ) = ( W cyclShift ( N + M ) ) )
7		2cshw	|- ( ( W e. Word V /\ M e. ZZ /\ N e. ZZ ) -> ( ( W cyclShift M ) cyclShift N ) = ( W cyclShift ( M + N ) ) )
8	7	3com23	|- ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( ( W cyclShift M ) cyclShift N ) = ( W cyclShift ( M + N ) ) )
9		2cshw	|- ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( ( W cyclShift N ) cyclShift M ) = ( W cyclShift ( N + M ) ) )
10	6 8 9	3eqtr4rd	|- ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( ( W cyclShift N ) cyclShift M ) = ( ( W cyclShift M ) cyclShift N ) )