Metamath Proof Explorer


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 ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ) = 𝐷 )