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