This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )