This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) )