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 e. Word X /\ B e. Word Y /\ ( W = ( A ++ B ) /\ W e. Word S ) ) -> A e. Word S )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( W = ( A ++ B ) -> ( W e. Word S <-> ( A ++ B ) e. Word S ) )
2		wrdv	|- ( A e. Word X -> A e. Word _V )
3		wrdv	|- ( B e. Word Y -> B e. Word _V )
4		ccatalpha	|- ( ( A e. Word _V /\ B e. Word _V ) -> ( ( A ++ B ) e. Word S <-> ( A e. Word S /\ B e. Word S ) ) )
5	2 3 4	syl2an	|- ( ( A e. Word X /\ B e. Word Y ) -> ( ( A ++ B ) e. Word S <-> ( A e. Word S /\ B e. Word S ) ) )
6	1 5	sylan9bbr	|- ( ( ( A e. Word X /\ B e. Word Y ) /\ W = ( A ++ B ) ) -> ( W e. Word S <-> ( A e. Word S /\ B e. Word S ) ) )
7		simpl	|- ( ( A e. Word S /\ B e. Word S ) -> A e. Word S )
8	6 7	biimtrdi	|- ( ( ( A e. Word X /\ B e. Word Y ) /\ W = ( A ++ B ) ) -> ( W e. Word S -> A e. Word S ) )
9	8	expimpd	|- ( ( A e. Word X /\ B e. Word Y ) -> ( ( W = ( A ++ B ) /\ W e. Word S ) -> A e. Word S ) )
10	9	3impia	|- ( ( A e. Word X /\ B e. Word Y /\ ( W = ( A ++ B ) /\ W e. Word S ) ) -> A e. Word S )