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