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 ) ) )