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

Metamath Proof Explorer

Theorem lswccats1

Description: The last symbol of a word concatenated with a singleton word is the symbol of the singleton word. (Contributed by AV, 6-Aug-2018) (Proof shortened by AV, 22-Oct-2018)

Ref Expression
Assertion lswccats1 ⊢ W ∈ Word V ∧ S ∈ V → lastS ⁡ W ++ ⟨“ S ”⟩ = S

Proof

Step Hyp Ref Expression
1 simpl ⊢ W ∈ Word V ∧ S ∈ V → W ∈ Word V
2 s1cl ⊢ S ∈ V → ⟨“ S ”⟩ ∈ Word V
3 2 adantl ⊢ W ∈ Word V ∧ S ∈ V → ⟨“ S ”⟩ ∈ Word V
4 s1nz ⊢ ⟨“ S ”⟩ ≠ ∅
5 4 a1i ⊢ W ∈ Word V ∧ S ∈ V → ⟨“ S ”⟩ ≠ ∅
6 lswccatn0lsw ⊢ W ∈ Word V ∧ ⟨“ S ”⟩ ∈ Word V ∧ ⟨“ S ”⟩ ≠ ∅ → lastS ⁡ W ++ ⟨“ S ”⟩ = lastS ⁡ ⟨“ S ”⟩
7 1 3 5 6 syl3anc ⊢ W ∈ Word V ∧ S ∈ V → lastS ⁡ W ++ ⟨“ S ”⟩ = lastS ⁡ ⟨“ S ”⟩
8 lsws1 ⊢ S ∈ V → lastS ⁡ ⟨“ S ”⟩ = S
9 8 adantl ⊢ W ∈ Word V ∧ S ∈ V → lastS ⁡ ⟨“ S ”⟩ = S
10 7 9 eqtrd ⊢ W ∈ Word V ∧ S ∈ V → lastS ⁡ W ++ ⟨“ S ”⟩ = S