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

Metamath Proof Explorer

Theorem lsws2

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

Ref Expression
Assertion lsws2 ( 𝐵 ∈ 𝑉 → ( lastS ‘ ⟨“ 𝐴 𝐵 ”⟩ ) = 𝐵 )

Proof

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