Theorem lsw1

Description: The last symbol of a word of length 1 is the first symbol of this word. (Contributed by Alexander van der Vekens, 19-Mar-2018)

	Ref	Expression
Assertion	lsw1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		lsw	⊢ ( 𝑊 ∈ Word 𝑉 → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
2		oveq1	⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( 1 − 1 ) )
3		1m1e0	⊢ ( 1 − 1 ) = 0
4	2 3	eqtrdi	⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( ( ♯ ‘ 𝑊 ) − 1 ) = 0 )
5	4	fveq2d	⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ 0 ) )
6	1 5	sylan9eq	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ 0 ) )