Theorem lsws1

Description: The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018)

	Ref	Expression
Assertion	lsws1	$$⊢A\in V\to \mathrm{lastS}\left(⟨“A”⟩\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		s1cl	$$⊢A\in V\to ⟨“A”⟩\in \mathrm{Word}V$$
2		s1len	$$⊢\left|⟨“A”⟩\right|=1$$
3		lsw1	$$⊢\left(⟨“A”⟩\in \mathrm{Word}V\wedge \left|⟨“A”⟩\right|=1\right)\to \mathrm{lastS}\left(⟨“A”⟩\right)=⟨“A”⟩\left(0\right)$$
4	1 2 3	sylancl	$$⊢A\in V\to \mathrm{lastS}\left(⟨“A”⟩\right)=⟨“A”⟩\left(0\right)$$
5		s1fv	$$⊢A\in V\to ⟨“A”⟩\left(0\right)=A$$
6	4 5	eqtrd	$$⊢A\in V\to \mathrm{lastS}\left(⟨“A”⟩\right)=A$$