This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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