Theorem s2s5

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

	Ref	Expression
Assertion	s2s5	$$⊢⟨“ABCDEFG”⟩=⟨“AB”⟩\mathrm{++}⟨“CDEFG”⟩$$

Proof

Step	Hyp	Ref	Expression
1		s1s2	$$⊢⟨“ABC”⟩=⟨“A”⟩\mathrm{++}⟨“BC”⟩$$
2	1	eqcomi	$$⊢⟨“A”⟩\mathrm{++}⟨“BC”⟩=⟨“ABC”⟩$$
3	2	oveq1i	$$⊢\left(⟨“A”⟩\mathrm{++}⟨“BC”⟩\right)\mathrm{++}⟨“DEFG”⟩=⟨“ABC”⟩\mathrm{++}⟨“DEFG”⟩$$
4		s1cli	$$⊢⟨“A”⟩\in \mathrm{Word}\mathrm{V}$$
5		s4cli	$$⊢⟨“DEFG”⟩\in \mathrm{Word}\mathrm{V}$$
6		df-s2	$$⊢⟨“AB”⟩=⟨“A”⟩\mathrm{++}⟨“B”⟩$$
7		s1s4	$$⊢⟨“CDEFG”⟩=⟨“C”⟩\mathrm{++}⟨“DEFG”⟩$$
8	4 5 6 7	cats2cat	$$⊢⟨“AB”⟩\mathrm{++}⟨“CDEFG”⟩=\left(⟨“A”⟩\mathrm{++}⟨“BC”⟩\right)\mathrm{++}⟨“DEFG”⟩$$
9		s3s4	$$⊢⟨“ABCDEFG”⟩=⟨“ABC”⟩\mathrm{++}⟨“DEFG”⟩$$
10	3 8 9	3eqtr4ri	$$⊢⟨“ABCDEFG”⟩=⟨“AB”⟩\mathrm{++}⟨“CDEFG”⟩$$