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	|- ( ( W e. Word V /\ ( # ` W ) = 1 ) -> ( lastS ` W ) = ( W ` 0 ) )

Proof

Step	Hyp	Ref	Expression
1		lsw	|- ( W e. Word V -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
2		oveq1	|- ( ( # ` W ) = 1 -> ( ( # ` W ) - 1 ) = ( 1 - 1 ) )
3		1m1e0	|- ( 1 - 1 ) = 0
4	2 3	eqtrdi	|- ( ( # ` W ) = 1 -> ( ( # ` W ) - 1 ) = 0 )
5	4	fveq2d	|- ( ( # ` W ) = 1 -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` 0 ) )
6	1 5	sylan9eq	|- ( ( W e. Word V /\ ( # ` W ) = 1 ) -> ( lastS ` W ) = ( W ` 0 ) )