Metamath Proof Explorer

Theorem s3s4

Description: Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021)

Ref Expression
Assertion s3s4 
|- <" A B C D E F G "> = ( <" A B C "> ++ <" D E F G "> )

Proof

Step Hyp Ref Expression
1 s2s2 
 |-  <" A B C D "> = ( <" A B "> ++ <" C D "> )
2 1 eqcomi 
 |-  ( <" A B "> ++ <" C D "> ) = <" A B C D ">
3 2 oveq1i 
 |-  ( ( <" A B "> ++ <" C D "> ) ++ <" E F G "> ) = ( <" A B C D "> ++ <" E F G "> )
4 s2cli 
 |-  <" A B "> e. Word _V
5 s3cli 
 |-  <" E F G "> e. Word _V
6 df-s3 
 |-  <" A B C "> = ( <" A B "> ++ <" C "> )
7 s1s3 
 |-  <" D E F G "> = ( <" D "> ++ <" E F G "> )
8 4 5 6 7 cats2cat 
 |-  ( <" A B C "> ++ <" D E F G "> ) = ( ( <" A B "> ++ <" C D "> ) ++ <" E F G "> )
9 s4s3 
 |-  <" A B C D E F G "> = ( <" A B C D "> ++ <" E F G "> )
10 3 8 9 3eqtr4ri 
 |-  <" A B C D E F G "> = ( <" A B C "> ++ <" D E F G "> )