Metamath Proof Explorer

Theorem lswcshw

Description: The last symbol of a word cyclically shifted by N positions is the symbol at index (N-1) of the original word. (Contributed by AV, 21-Mar-2018) (Revised by AV, 5-Jun-2018) (Revised by AV, 1-Nov-2018)

Ref Expression
Assertion lswcshw 
|- ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W cyclShift N ) ) = ( W ` ( N - 1 ) ) )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( W cyclShift N ) e. _V
2 lsw 
 |-  ( ( W cyclShift N ) e. _V -> ( lastS ` ( W cyclShift N ) ) = ( ( W cyclShift N ) ` ( ( # ` ( W cyclShift N ) ) - 1 ) ) )
3 1 2 mp1i 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W cyclShift N ) ) = ( ( W cyclShift N ) ` ( ( # ` ( W cyclShift N ) ) - 1 ) ) )
4 elfzelz 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> N e. ZZ )
5 cshwlen 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )
6 4 5 sylan2 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )
7 6 fvoveq1d 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` ( W cyclShift N ) ) - 1 ) ) = ( ( W cyclShift N ) ` ( ( # ` W ) - 1 ) ) )
8 cshwidxn 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( ( # ` W ) - 1 ) ) = ( W ` ( N - 1 ) ) )
9 3 7 8 3eqtrd 
 |-  ( ( W e. Word V /\ N e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W cyclShift N ) ) = ( W ` ( N - 1 ) ) )