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

Metamath Proof Explorer

Theorem cats1cat

Description: Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Hypotheses cats1cld.1 ⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
cats1cat.2 ⊢ 𝐴 ∈ Word V
cats1cat.3 ⊢ 𝑆 ∈ Word V
cats1cat.4 ⊢ 𝐶 = ( 𝐵 ++ ⟨“ 𝑋 ”⟩ )
cats1cat.5 ⊢ 𝐵 = ( 𝐴 ++ 𝑆 )
Assertion cats1cat 𝐶 = ( 𝐴 ++ 𝑇 )

Proof

Step Hyp Ref Expression
1 cats1cld.1 ⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
2 cats1cat.2 ⊢ 𝐴 ∈ Word V
3 cats1cat.3 ⊢ 𝑆 ∈ Word V
4 cats1cat.4 ⊢ 𝐶 = ( 𝐵 ++ ⟨“ 𝑋 ”⟩ )
5 cats1cat.5 ⊢ 𝐵 = ( 𝐴 ++ 𝑆 )
6 5 oveq1i ⊢ ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) = ( ( 𝐴 ++ 𝑆 ) ++ ⟨“ 𝑋 ”⟩ )
7 s1cli ⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
8 ccatass ⊢ ( ( 𝐴 ∈ Word V ∧ 𝑆 ∈ Word V ∧ ⟨“ 𝑋 ”⟩ ∈ Word V ) → ( ( 𝐴 ++ 𝑆 ) ++ ⟨“ 𝑋 ”⟩ ) = ( 𝐴 ++ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ) )
9 2 3 7 8 mp3an ⊢ ( ( 𝐴 ++ 𝑆 ) ++ ⟨“ 𝑋 ”⟩ ) = ( 𝐴 ++ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) )
10 6 9 eqtri ⊢ ( 𝐵 ++ ⟨“ 𝑋 ”⟩ ) = ( 𝐴 ++ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) )
11 1 oveq2i ⊢ ( 𝐴 ++ 𝑇 ) = ( 𝐴 ++ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) )
12 10 4 11 3eqtr4i ⊢ 𝐶 = ( 𝐴 ++ 𝑇 )