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 ∈ Word V ∧ N ∈ 1 … W → lastS ⁡ W cyclShift N = W ⁡ N − 1

Proof

Step Hyp Ref Expression
1 ovex ⊢ W cyclShift N ∈ V
2 lsw ⊢ W cyclShift N ∈ V → lastS ⁡ W cyclShift N = W cyclShift N ⁡ W cyclShift N − 1
3 1 2 mp1i ⊢ W ∈ Word V ∧ N ∈ 1 … W → lastS ⁡ W cyclShift N = W cyclShift N ⁡ W cyclShift N − 1
4 elfzelz ⊢ N ∈ 1 … W → N ∈ ℤ
5 cshwlen ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W
6 4 5 sylan2 ⊢ W ∈ Word V ∧ N ∈ 1 … W → W cyclShift N = W
7 6 fvoveq1d ⊢ W ∈ Word V ∧ N ∈ 1 … W → W cyclShift N ⁡ W cyclShift N − 1 = W cyclShift N ⁡ W − 1
8 cshwidxn ⊢ W ∈ Word V ∧ N ∈ 1 … W → W cyclShift N ⁡ W − 1 = W ⁡ N − 1
9 3 7 8 3eqtrd ⊢ W ∈ Word V ∧ N ∈ 1 … W → lastS ⁡ W cyclShift N = W ⁡ N − 1