Theorem s3s4

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

	Ref	Expression
Assertion	s3s4	$$⊢⟨“ABCDEFG”⟩=⟨“ABC”⟩\mathrm{++}⟨“DEFG”⟩$$

Proof

Step	Hyp	Ref	Expression
1		s2s2	$$⊢⟨“ABCD”⟩=⟨“AB”⟩\mathrm{++}⟨“CD”⟩$$
2	1	eqcomi	$$⊢⟨“AB”⟩\mathrm{++}⟨“CD”⟩=⟨“ABCD”⟩$$
3	2	oveq1i	$$⊢\left(⟨“AB”⟩\mathrm{++}⟨“CD”⟩\right)\mathrm{++}⟨“EFG”⟩=⟨“ABCD”⟩\mathrm{++}⟨“EFG”⟩$$
4		s2cli	$$⊢⟨“AB”⟩\in \mathrm{Word}\mathrm{V}$$
5		s3cli	$$⊢⟨“EFG”⟩\in \mathrm{Word}\mathrm{V}$$
6		df-s3	$$⊢⟨“ABC”⟩=⟨“AB”⟩\mathrm{++}⟨“C”⟩$$
7		s1s3	$$⊢⟨“DEFG”⟩=⟨“D”⟩\mathrm{++}⟨“EFG”⟩$$
8	4 5 6 7	cats2cat	$$⊢⟨“ABC”⟩\mathrm{++}⟨“DEFG”⟩=\left(⟨“AB”⟩\mathrm{++}⟨“CD”⟩\right)\mathrm{++}⟨“EFG”⟩$$
9		s4s3	$$⊢⟨“ABCDEFG”⟩=⟨“ABCD”⟩\mathrm{++}⟨“EFG”⟩$$
10	3 8 9	3eqtr4ri	$$⊢⟨“ABCDEFG”⟩=⟨“ABC”⟩\mathrm{++}⟨“DEFG”⟩$$