Metamath Proof Explorer

Theorem lsws3

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

Ref Expression
Assertion lsws3 ⊢ C ∈ V → lastS ⁡ ⟨“ ABC ”⟩ = C

Proof

Step Hyp Ref Expression
1 s3cli ⊢ ⟨“ ABC ”⟩ ∈ Word V
2 lsw ⊢ ⟨“ ABC ”⟩ ∈ Word V → lastS ⁡ ⟨“ ABC ”⟩ = ⟨“ ABC ”⟩ ⁡ ⟨“ ABC ”⟩ − 1
3 1 2 mp1i ⊢ C ∈ V → lastS ⁡ ⟨“ ABC ”⟩ = ⟨“ ABC ”⟩ ⁡ ⟨“ ABC ”⟩ − 1
4 s3len ⊢ ⟨“ ABC ”⟩ = 3
5 4 oveq1i ⊢ ⟨“ ABC ”⟩ − 1 = 3 − 1
6 3m1e2 ⊢ 3 − 1 = 2
7 5 6 eqtri ⊢ ⟨“ ABC ”⟩ − 1 = 2
8 7 fveq2i ⊢ ⟨“ ABC ”⟩ ⁡ ⟨“ ABC ”⟩ − 1 = ⟨“ ABC ”⟩ ⁡ 2
9 8 a1i ⊢ C ∈ V → ⟨“ ABC ”⟩ ⁡ ⟨“ ABC ”⟩ − 1 = ⟨“ ABC ”⟩ ⁡ 2
10 s3fv2 ⊢ C ∈ V → ⟨“ ABC ”⟩ ⁡ 2 = C
11 3 9 10 3eqtrd ⊢ C ∈ V → lastS ⁡ ⟨“ ABC ”⟩ = C