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 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 )