Metamath Proof Explorer

Theorem ccatrcl1

Description: Reverse closure of a concatenation: If the concatenation of two arbitrary words is a word over an alphabet then the symbols of the first word belong to the alphabet. (Contributed by AV, 3-Mar-2021)

		Ref	Expression
	Assertion	ccatrcl1	$⊢ (A \in Word X \land B \in Word Y \land (W = A ++ B \land W \in Word S)) \to A \in Word S$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ W = A ++ B \to (W \in Word S \leftrightarrow A ++ B \in Word S)$
2		wrdv	$⊢ A \in Word X \to A \in Word V$
3		wrdv	$⊢ B \in Word Y \to B \in Word V$
4		ccatalpha	$⊢ (A \in Word V \land B \in Word V) \to (A ++ B \in Word S \leftrightarrow (A \in Word S \land B \in Word S))$
5	2 3 4	syl2an	$⊢ (A \in Word X \land B \in Word Y) \to (A ++ B \in Word S \leftrightarrow (A \in Word S \land B \in Word S))$
6	1 5	sylan9bbr	$⊢ ((A \in Word X \land B \in Word Y) \land W = A ++ B) \to (W \in Word S \leftrightarrow (A \in Word S \land B \in Word S))$
7		simpl	$⊢ (A \in Word S \land B \in Word S) \to A \in Word S$
8	6 7	biimtrdi	$⊢ ((A \in Word X \land B \in Word Y) \land W = A ++ B) \to (W \in Word S \to A \in Word S)$
9	8	expimpd	$⊢ (A \in Word X \land B \in Word Y) \to ((W = A ++ B \land W \in Word S) \to A \in Word S)$
10	9	3impia	$⊢ (A \in Word X \land B \in Word Y \land (W = A ++ B \land W \in Word S)) \to A \in Word S$