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	⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ ( 𝑊 = ( 𝐴 ++ 𝐵 ) ∧ 𝑊 ∈ Word 𝑆 ) ) → 𝐴 ∈ Word 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑊 = ( 𝐴 ++ 𝐵 ) → ( 𝑊 ∈ Word 𝑆 ↔ ( 𝐴 ++ 𝐵 ) ∈ Word 𝑆 ) )
2		wrdv	⊢ ( 𝐴 ∈ Word 𝑋 → 𝐴 ∈ Word V )
3		wrdv	⊢ ( 𝐵 ∈ Word 𝑌 → 𝐵 ∈ Word V )
4		ccatalpha	⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑆 ↔ ( 𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ) ) )
5	2 3 4	syl2an	⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ) → ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑆 ↔ ( 𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ) ) )
6	1 5	sylan9bbr	⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ) ∧ 𝑊 = ( 𝐴 ++ 𝐵 ) ) → ( 𝑊 ∈ Word 𝑆 ↔ ( 𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ) ) )
7		simpl	⊢ ( ( 𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ) → 𝐴 ∈ Word 𝑆 )
8	6 7	biimtrdi	⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ) ∧ 𝑊 = ( 𝐴 ++ 𝐵 ) ) → ( 𝑊 ∈ Word 𝑆 → 𝐴 ∈ Word 𝑆 ) )
9	8	expimpd	⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ) → ( ( 𝑊 = ( 𝐴 ++ 𝐵 ) ∧ 𝑊 ∈ Word 𝑆 ) → 𝐴 ∈ Word 𝑆 ) )
10	9	3impia	⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ ( 𝑊 = ( 𝐴 ++ 𝐵 ) ∧ 𝑊 ∈ Word 𝑆 ) ) → 𝐴 ∈ Word 𝑆 )