Theorem lsws4

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

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

Proof

Step	Hyp	Ref	Expression
1		s4cli	$$⊢⟨“ABCD”⟩\in \mathrm{Word}\mathrm{V}$$
2		lsw	$$⊢⟨“ABCD”⟩\in \mathrm{Word}\mathrm{V}\to \mathrm{lastS}\left(⟨“ABCD”⟩\right)=⟨“ABCD”⟩\left(\left|⟨“ABCD”⟩\right|-1\right)$$
3	1 2	mp1i	$$⊢D\in V\to \mathrm{lastS}\left(⟨“ABCD”⟩\right)=⟨“ABCD”⟩\left(\left|⟨“ABCD”⟩\right|-1\right)$$
4		s4len	$$⊢\left|⟨“ABCD”⟩\right|=4$$
5	4	oveq1i	$$⊢\left|⟨“ABCD”⟩\right|-1=4-1$$
6		4m1e3	$$⊢4-1=3$$
7	5 6	eqtri	$$⊢\left|⟨“ABCD”⟩\right|-1=3$$
8	7	fveq2i	$$⊢⟨“ABCD”⟩\left(\left|⟨“ABCD”⟩\right|-1\right)=⟨“ABCD”⟩\left(3\right)$$
9	8	a1i	$$⊢D\in V\to ⟨“ABCD”⟩\left(\left|⟨“ABCD”⟩\right|-1\right)=⟨“ABCD”⟩\left(3\right)$$
10		s4fv3	$$⊢D\in V\to ⟨“ABCD”⟩\left(3\right)=D$$
11	3 9 10	3eqtrd	$$⊢D\in V\to \mathrm{lastS}\left(⟨“ABCD”⟩\right)=D$$