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 WWordVN1WlastSWcyclShiftN=WN1

Proof

Step Hyp Ref Expression
1 ovex WcyclShiftNV
2 lsw WcyclShiftNVlastSWcyclShiftN=WcyclShiftNWcyclShiftN1
3 1 2 mp1i WWordVN1WlastSWcyclShiftN=WcyclShiftNWcyclShiftN1
4 elfzelz N1WN
5 cshwlen WWordVNWcyclShiftN=W
6 4 5 sylan2 WWordVN1WWcyclShiftN=W
7 6 fvoveq1d WWordVN1WWcyclShiftNWcyclShiftN1=WcyclShiftNW1
8 cshwidxn WWordVN1WWcyclShiftNW1=WN1
9 3 7 8 3eqtrd WWordVN1WlastSWcyclShiftN=WN1