Theorem lsws3

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

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

Proof

Step	Hyp	Ref	Expression
1		s3cli	$$⊢⟨“ABC”⟩\in \mathrm{Word}\mathrm{V}$$
2		lsw	$$⊢⟨“ABC”⟩\in \mathrm{Word}\mathrm{V}\to \mathrm{lastS}\left(⟨“ABC”⟩\right)=⟨“ABC”⟩\left(\left|⟨“ABC”⟩\right|-1\right)$$
3	1 2	mp1i	$$⊢C\in V\to \mathrm{lastS}\left(⟨“ABC”⟩\right)=⟨“ABC”⟩\left(\left|⟨“ABC”⟩\right|-1\right)$$
4		s3len	$$⊢\left|⟨“ABC”⟩\right|=3$$
5	4	oveq1i	$$⊢\left|⟨“ABC”⟩\right|-1=3-1$$
6		3m1e2	$$⊢3-1=2$$
7	5 6	eqtri	$$⊢\left|⟨“ABC”⟩\right|-1=2$$
8	7	fveq2i	$$⊢⟨“ABC”⟩\left(\left|⟨“ABC”⟩\right|-1\right)=⟨“ABC”⟩\left(2\right)$$
9	8	a1i	$$⊢C\in V\to ⟨“ABC”⟩\left(\left|⟨“ABC”⟩\right|-1\right)=⟨“ABC”⟩\left(2\right)$$
10		s3fv2	$$⊢C\in V\to ⟨“ABC”⟩\left(2\right)=C$$
11	3 9 10	3eqtrd	$$⊢C\in V\to \mathrm{lastS}\left(⟨“ABC”⟩\right)=C$$