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 e. Word _V
	cats1cat.3	|- S e. 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 e. Word _V
3		cats1cat.3	|- S e. 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 "> e. Word _V
8		ccatass	|- ( ( A e. Word _V /\ S e. Word _V /\ <" X "> e. 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 )