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 \in Word V \land S \in V) \to lastS (W ++ ⟨“ S ”⟩) = S$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (W \in Word V \land S \in V) \to W \in Word V$
2		s1cl	$⊢ S \in V \to ⟨“ S ”⟩ \in Word V$
3	2	adantl	$⊢ (W \in Word V \land S \in V) \to ⟨“ S ”⟩ \in Word V$
4		s1nz	$⊢ ⟨“ S ”⟩ \neq \emptyset$
5	4	a1i	$⊢ (W \in Word V \land S \in V) \to ⟨“ S ”⟩ \neq \emptyset$
6		lswccatn0lsw	$⊢ (W \in Word V \land ⟨“ S ”⟩ \in Word V \land ⟨“ S ”⟩ \neq \emptyset) \to lastS (W ++ ⟨“ S ”⟩) = lastS (⟨“ S ”⟩)$
7	1 3 5 6	syl3anc	$⊢ (W \in Word V \land S \in V) \to lastS (W ++ ⟨“ S ”⟩) = lastS (⟨“ S ”⟩)$
8		lsws1	$⊢ S \in V \to lastS (⟨“ S ”⟩) = S$
9	8	adantl	$⊢ (W \in Word V \land S \in V) \to lastS (⟨“ S ”⟩) = S$
10	7 9	eqtrd	$⊢ (W \in Word V \land S \in V) \to lastS (W ++ ⟨“ S ”⟩) = S$