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	⊢ ( 𝐷 ∈ 𝑉 → ( lastS ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) = 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		s4cli	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∈ Word V
2		lsw	⊢ ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∈ Word V → ( lastS ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) − 1 ) ) )
3	1 2	mp1i	⊢ ( 𝐷 ∈ 𝑉 → ( lastS ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) − 1 ) ) )
4		s4len	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) = 4
5	4	oveq1i	⊢ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) − 1 ) = ( 4 − 1 )
6		4m1e3	⊢ ( 4 − 1 ) = 3
7	5 6	eqtri	⊢ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) − 1 ) = 3
8	7	fveq2i	⊢ ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) − 1 ) ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 )
9	8	a1i	⊢ ( 𝐷 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) − 1 ) ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) )
10		s4fv3	⊢ ( 𝐷 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) = 𝐷 )
11	3 9 10	3eqtrd	⊢ ( 𝐷 ∈ 𝑉 → ( lastS ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) = 𝐷 )