# Metamath Proof Explorer

## Theorem s5s2

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

Ref Expression
Assertion s5s2 ${⊢}⟨“{A}{B}{C}{D}{E}{F}{G}”⟩=⟨“{A}{B}{C}{D}{E}”⟩\mathrm{++}⟨“{F}{G}”⟩$

### Proof

Step Hyp Ref Expression
1 s4s2 ${⊢}⟨“{A}{B}{C}{D}{E}{F}”⟩=⟨“{A}{B}{C}{D}”⟩\mathrm{++}⟨“{E}{F}”⟩$
2 1 eqcomi ${⊢}⟨“{A}{B}{C}{D}”⟩\mathrm{++}⟨“{E}{F}”⟩=⟨“{A}{B}{C}{D}{E}{F}”⟩$
3 2 oveq1i ${⊢}\left(⟨“{A}{B}{C}{D}”⟩\mathrm{++}⟨“{E}{F}”⟩\right)\mathrm{++}⟨“{G}”⟩=⟨“{A}{B}{C}{D}{E}{F}”⟩\mathrm{++}⟨“{G}”⟩$
4 s4cli ${⊢}⟨“{A}{B}{C}{D}”⟩\in \mathrm{Word}\mathrm{V}$
5 s1cli ${⊢}⟨“{G}”⟩\in \mathrm{Word}\mathrm{V}$
6 df-s5 ${⊢}⟨“{A}{B}{C}{D}{E}”⟩=⟨“{A}{B}{C}{D}”⟩\mathrm{++}⟨“{E}”⟩$
7 df-s2 ${⊢}⟨“{F}{G}”⟩=⟨“{F}”⟩\mathrm{++}⟨“{G}”⟩$
8 4 5 6 7 cats2cat ${⊢}⟨“{A}{B}{C}{D}{E}”⟩\mathrm{++}⟨“{F}{G}”⟩=\left(⟨“{A}{B}{C}{D}”⟩\mathrm{++}⟨“{E}{F}”⟩\right)\mathrm{++}⟨“{G}”⟩$
9 df-s7 ${⊢}⟨“{A}{B}{C}{D}{E}{F}{G}”⟩=⟨“{A}{B}{C}{D}{E}{F}”⟩\mathrm{++}⟨“{G}”⟩$
10 3 8 9 3eqtr4ri ${⊢}⟨“{A}{B}{C}{D}{E}{F}{G}”⟩=⟨“{A}{B}{C}{D}{E}”⟩\mathrm{++}⟨“{F}{G}”⟩$