Theorem s5s2

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

	Ref	Expression
Assertion	s5s2	$$⊢⟨“ABCDEFG”⟩=⟨“ABCDE”⟩\mathrm{++}⟨“FG”⟩$$

Proof

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