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

Metamath Proof Explorer

Theorem 3cshw

Description: Cyclically shifting a word three times results in a once cyclically shifted word under certain circumstances. (Contributed by AV, 6-Jun-2018) (Revised by AV, 1-Nov-2018)

Ref Expression
Assertion 3cshw 
|- ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( W cyclShift N ) = ( ( ( W cyclShift M ) cyclShift N ) cyclShift ( ( # ` W ) - M ) ) )

Proof

Step Hyp Ref Expression
1 2cshwid 
 |-  ( ( W e. Word V /\ M e. ZZ ) -> ( ( W cyclShift M ) cyclShift ( ( # ` W ) - M ) ) = W )
2 1 3adant2 
 |-  ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( ( W cyclShift M ) cyclShift ( ( # ` W ) - M ) ) = W )
3 2 eqcomd 
 |-  ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> W = ( ( W cyclShift M ) cyclShift ( ( # ` W ) - M ) ) )
4 3 oveq1d 
 |-  ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( W cyclShift N ) = ( ( ( W cyclShift M ) cyclShift ( ( # ` W ) - M ) ) cyclShift N ) )
5 cshwcl 
 |-  ( W e. Word V -> ( W cyclShift M ) e. Word V )
6 5 3ad2ant1 
 |-  ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( W cyclShift M ) e. Word V )
7 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
8 7 nn0zd 
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
9 zsubcl 
 |-  ( ( ( # ` W ) e. ZZ /\ M e. ZZ ) -> ( ( # ` W ) - M ) e. ZZ )
10 8 9 sylan 
 |-  ( ( W e. Word V /\ M e. ZZ ) -> ( ( # ` W ) - M ) e. ZZ )
11 10 3adant2 
 |-  ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( ( # ` W ) - M ) e. ZZ )
12 simp2 
 |-  ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> N e. ZZ )
13 2cshwcom 
 |-  ( ( ( W cyclShift M ) e. Word V /\ ( ( # ` W ) - M ) e. ZZ /\ N e. ZZ ) -> ( ( ( W cyclShift M ) cyclShift ( ( # ` W ) - M ) ) cyclShift N ) = ( ( ( W cyclShift M ) cyclShift N ) cyclShift ( ( # ` W ) - M ) ) )
14 6 11 12 13 syl3anc 
 |-  ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( ( ( W cyclShift M ) cyclShift ( ( # ` W ) - M ) ) cyclShift N ) = ( ( ( W cyclShift M ) cyclShift N ) cyclShift ( ( # ` W ) - M ) ) )
15 4 14 eqtrd 
 |-  ( ( W e. Word V /\ N e. ZZ /\ M e. ZZ ) -> ( W cyclShift N ) = ( ( ( W cyclShift M ) cyclShift N ) cyclShift ( ( # ` W ) - M ) ) )