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	$$⊢\left(W\in \mathrm{Word}V\wedge \left|W\right|=1\right)\to \mathrm{lastS}\left(W\right)=W\left(0\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsw	$$⊢W\in \mathrm{Word}V\to \mathrm{lastS}\left(W\right)=W\left(\left|W\right|-1\right)$$
2		oveq1	$$⊢\left|W\right|=1\to \left|W\right|-1=1-1$$
3		1m1e0	$$⊢1-1=0$$
4	2 3	eqtrdi	$$⊢\left|W\right|=1\to \left|W\right|-1=0$$
5	4	fveq2d	$$⊢\left|W\right|=1\to W\left(\left|W\right|-1\right)=W\left(0\right)$$
6	1 5	sylan9eq	$$⊢\left(W\in \mathrm{Word}V\wedge \left|W\right|=1\right)\to \mathrm{lastS}\left(W\right)=W\left(0\right)$$