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 ⊢ D ∈ V → lastS ⁡ ⟨“ ABCD ”⟩ = D

Proof

Step Hyp Ref Expression
1 s4cli ⊢ ⟨“ ABCD ”⟩ ∈ Word V
2 lsw ⊢ ⟨“ ABCD ”⟩ ∈ Word V → lastS ⁡ ⟨“ ABCD ”⟩ = ⟨“ ABCD ”⟩ ⁡ ⟨“ ABCD ”⟩ − 1
3 1 2 mp1i ⊢ D ∈ V → lastS ⁡ ⟨“ ABCD ”⟩ = ⟨“ ABCD ”⟩ ⁡ ⟨“ ABCD ”⟩ − 1
4 s4len ⊢ ⟨“ ABCD ”⟩ = 4
5 4 oveq1i ⊢ ⟨“ ABCD ”⟩ − 1 = 4 − 1
6 4m1e3 ⊢ 4 − 1 = 3
7 5 6 eqtri ⊢ ⟨“ ABCD ”⟩ − 1 = 3
8 7 fveq2i ⊢ ⟨“ ABCD ”⟩ ⁡ ⟨“ ABCD ”⟩ − 1 = ⟨“ ABCD ”⟩ ⁡ 3
9 8 a1i ⊢ D ∈ V → ⟨“ ABCD ”⟩ ⁡ ⟨“ ABCD ”⟩ − 1 = ⟨“ ABCD ”⟩ ⁡ 3
10 s4fv3 ⊢ D ∈ V → ⟨“ ABCD ”⟩ ⁡ 3 = D
11 3 9 10 3eqtrd ⊢ D ∈ V → lastS ⁡ ⟨“ ABCD ”⟩ = D