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

Metamath Proof Explorer

Theorem lswccat0lsw

Description: The last symbol of a word concatenated with the empty word is the last symbol of the word. (Contributed by AV, 22-Oct-2018) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion lswccat0lsw ⊢ W ∈ Word V → lastS ⁡ W ++ ∅ = lastS ⁡ W

Proof

Step Hyp Ref Expression
1 ccatrid ⊢ W ∈ Word V → W ++ ∅ = W
2 1 fveq2d ⊢ W ∈ Word V → lastS ⁡ W ++ ∅ = lastS ⁡ W