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	⊢ 𝐶 = ( 𝐴 ++ 𝑇 )