This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 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 𝑆 )