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 ⊢ T = S ++ ⟨“ X ”⟩
cats1cat.2 ⊢ A ∈ Word V
cats1cat.3 ⊢ S ∈ Word V
cats1cat.4 ⊢ C = B ++ ⟨“ X ”⟩
cats1cat.5 ⊢ B = A ++ S
Assertion cats1cat ⊢ C = A ++ T

Proof

Step Hyp Ref Expression
1 cats1cld.1 ⊢ T = S ++ ⟨“ X ”⟩
2 cats1cat.2 ⊢ A ∈ Word V
3 cats1cat.3 ⊢ S ∈ Word V
4 cats1cat.4 ⊢ C = B ++ ⟨“ X ”⟩
5 cats1cat.5 ⊢ B = A ++ S
6 5 oveq1i ⊢ B ++ ⟨“ X ”⟩ = A ++ S ++ ⟨“ X ”⟩
7 s1cli ⊢ ⟨“ X ”⟩ ∈ Word V
8 ccatass ⊢ A ∈ Word V ∧ S ∈ Word V ∧ ⟨“ X ”⟩ ∈ Word V → A ++ S ++ ⟨“ X ”⟩ = A ++ S ++ ⟨“ X ”⟩
9 2 3 7 8 mp3an ⊢ A ++ S ++ ⟨“ X ”⟩ = A ++ S ++ ⟨“ X ”⟩
10 6 9 eqtri ⊢ B ++ ⟨“ X ”⟩ = A ++ S ++ ⟨“ X ”⟩
11 1 oveq2i ⊢ A ++ T = A ++ S ++ ⟨“ X ”⟩
12 10 4 11 3eqtr4i ⊢ C = A ++ T