Metamath Proof Explorer

Theorem ccatws1ls

Description: The last symbol of the concatenation of a word with a singleton word is the symbol of the singleton word. (Contributed by AV, 29-Sep-2018) (Proof shortened by AV, 14-Oct-2018)

		Ref	Expression
	Assertion	ccatws1ls	$⊢ (W \in Word V \land X \in V) \to (W ++ ⟨“ X ”⟩) (\|W\|) = X$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$⊢ (W \in Word V \land X \in V) \to \|W\| = \|W\|$
2		ccats1val2	$⊢ (W \in Word V \land X \in V \land \|W\| = \|W\|) \to (W ++ ⟨“ X ”⟩) (\|W\|) = X$
3	1 2	mpd3an3	$⊢ (W \in Word V \land X \in V) \to (W ++ ⟨“ X ”⟩) (\|W\|) = X$