Theorem lsws2

Description: The last symbol of a doubleton word is its second symbol. (Contributed by AV, 8-Feb-2021)

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

Proof

Step	Hyp	Ref	Expression
1		s2cli	$$⊢⟨“AB”⟩\in \mathrm{Word}\mathrm{V}$$
2		lsw	$$⊢⟨“AB”⟩\in \mathrm{Word}\mathrm{V}\to \mathrm{lastS}\left(⟨“AB”⟩\right)=⟨“AB”⟩\left(\left|⟨“AB”⟩\right|-1\right)$$
3	1 2	mp1i	$$⊢B\in V\to \mathrm{lastS}\left(⟨“AB”⟩\right)=⟨“AB”⟩\left(\left|⟨“AB”⟩\right|-1\right)$$
4		s2len	$$⊢\left|⟨“AB”⟩\right|=2$$
5	4	oveq1i	$$⊢\left|⟨“AB”⟩\right|-1=2-1$$
6		2m1e1	$$⊢2-1=1$$
7	5 6	eqtri	$$⊢\left|⟨“AB”⟩\right|-1=1$$
8	7	fveq2i	$$⊢⟨“AB”⟩\left(\left|⟨“AB”⟩\right|-1\right)=⟨“AB”⟩\left(1\right)$$
9	8	a1i	$$⊢B\in V\to ⟨“AB”⟩\left(\left|⟨“AB”⟩\right|-1\right)=⟨“AB”⟩\left(1\right)$$
10		s2fv1	$$⊢B\in V\to ⟨“AB”⟩\left(1\right)=B$$
11	3 9 10	3eqtrd	$$⊢B\in V\to \mathrm{lastS}\left(⟨“AB”⟩\right)=B$$