Theorem cats1cat

Description: Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Hypotheses	cats1cld.1	$$⊢T=S\mathrm{++}⟨“X”⟩$$
	cats1cat.2	$$⊢A\in \mathrm{Word}\mathrm{V}$$
	cats1cat.3	$$⊢S\in \mathrm{Word}\mathrm{V}$$
	cats1cat.4	$$⊢C=B\mathrm{++}⟨“X”⟩$$
	cats1cat.5	$$⊢B=A\mathrm{++}S$$
Assertion	cats1cat	$$⊢C=A\mathrm{++}T$$

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	$$⊢T=S\mathrm{++}⟨“X”⟩$$
2		cats1cat.2	$$⊢A\in \mathrm{Word}\mathrm{V}$$
3		cats1cat.3	$$⊢S\in \mathrm{Word}\mathrm{V}$$
4		cats1cat.4	$$⊢C=B\mathrm{++}⟨“X”⟩$$
5		cats1cat.5	$$⊢B=A\mathrm{++}S$$
6	5	oveq1i	$$⊢B\mathrm{++}⟨“X”⟩=\left(A\mathrm{++}S\right)\mathrm{++}⟨“X”⟩$$
7		s1cli	$$⊢⟨“X”⟩\in \mathrm{Word}\mathrm{V}$$
8		ccatass	$$⊢\left(A\in \mathrm{Word}\mathrm{V}\wedge S\in \mathrm{Word}\mathrm{V}\wedge ⟨“X”⟩\in \mathrm{Word}\mathrm{V}\right)\to \left(A\mathrm{++}S\right)\mathrm{++}⟨“X”⟩=A\mathrm{++}\left(S\mathrm{++}⟨“X”⟩\right)$$
9	2 3 7 8	mp3an	$$⊢\left(A\mathrm{++}S\right)\mathrm{++}⟨“X”⟩=A\mathrm{++}\left(S\mathrm{++}⟨“X”⟩\right)$$
10	6 9	eqtri	$$⊢B\mathrm{++}⟨“X”⟩=A\mathrm{++}\left(S\mathrm{++}⟨“X”⟩\right)$$
11	1	oveq2i	$$⊢A\mathrm{++}T=A\mathrm{++}\left(S\mathrm{++}⟨“X”⟩\right)$$
12	10 4 11	3eqtr4i	$$⊢C=A\mathrm{++}T$$