Metamath Proof Explorer


Theorem cats2cat

Description: Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021)

Ref Expression
Hypotheses cats2cat.b
|- B e. Word _V
cats2cat.d
|- D e. Word _V
cats2cat.a
|- A = ( B ++ <" X "> )
cats2cat.c
|- C = ( <" Y "> ++ D )
Assertion cats2cat
|- ( A ++ C ) = ( ( B ++ <" X Y "> ) ++ D )

Proof

Step Hyp Ref Expression
1 cats2cat.b
 |-  B e. Word _V
2 cats2cat.d
 |-  D e. Word _V
3 cats2cat.a
 |-  A = ( B ++ <" X "> )
4 cats2cat.c
 |-  C = ( <" Y "> ++ D )
5 3 4 oveq12i
 |-  ( A ++ C ) = ( ( B ++ <" X "> ) ++ ( <" Y "> ++ D ) )
6 s1cli
 |-  <" X "> e. Word _V
7 ccatcl
 |-  ( ( B e. Word _V /\ <" X "> e. Word _V ) -> ( B ++ <" X "> ) e. Word _V )
8 1 6 7 mp2an
 |-  ( B ++ <" X "> ) e. Word _V
9 s1cli
 |-  <" Y "> e. Word _V
10 ccatass
 |-  ( ( ( B ++ <" X "> ) e. Word _V /\ <" Y "> e. Word _V /\ D e. Word _V ) -> ( ( ( B ++ <" X "> ) ++ <" Y "> ) ++ D ) = ( ( B ++ <" X "> ) ++ ( <" Y "> ++ D ) ) )
11 8 9 2 10 mp3an
 |-  ( ( ( B ++ <" X "> ) ++ <" Y "> ) ++ D ) = ( ( B ++ <" X "> ) ++ ( <" Y "> ++ D ) )
12 ccatass
 |-  ( ( B e. Word _V /\ <" X "> e. Word _V /\ <" Y "> e. Word _V ) -> ( ( B ++ <" X "> ) ++ <" Y "> ) = ( B ++ ( <" X "> ++ <" Y "> ) ) )
13 1 6 9 12 mp3an
 |-  ( ( B ++ <" X "> ) ++ <" Y "> ) = ( B ++ ( <" X "> ++ <" Y "> ) )
14 df-s2
 |-  <" X Y "> = ( <" X "> ++ <" Y "> )
15 14 eqcomi
 |-  ( <" X "> ++ <" Y "> ) = <" X Y ">
16 15 oveq2i
 |-  ( B ++ ( <" X "> ++ <" Y "> ) ) = ( B ++ <" X Y "> )
17 13 16 eqtri
 |-  ( ( B ++ <" X "> ) ++ <" Y "> ) = ( B ++ <" X Y "> )
18 17 oveq1i
 |-  ( ( ( B ++ <" X "> ) ++ <" Y "> ) ++ D ) = ( ( B ++ <" X Y "> ) ++ D )
19 5 11 18 3eqtr2i
 |-  ( A ++ C ) = ( ( B ++ <" X Y "> ) ++ D )