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

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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 ovex ⊢ ( 𝑊 cyclShift 𝑁 ) ∈ V
2 lsw ⊢ ( ( 𝑊 cyclShift 𝑁 ) ∈ V → ( lastS ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) − 1 ) ) )
3 1 2 mp1i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) − 1 ) ) )
4 elfzelz ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℤ )
5 cshwlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
6 4 5 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
7 6 fvoveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) − 1 ) ) = ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
8 cshwidxn ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )
9 3 7 8 3eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )