Theorem cats1co

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

	Ref	Expression
Hypotheses	cats1cld.1	$$⊢T=S\mathrm{++}⟨“X”⟩$$
	cats1cld.2	$$⊢\phi \to S\in \mathrm{Word}A$$
	cats1cld.3	$$⊢\phi \to X\in A$$
	cats1co.4	$$⊢\phi \to F:A⟶B$$
	cats1co.5	$$⊢\phi \to F\circ S=U$$
	cats1co.6	$$⊢V=U\mathrm{++}⟨“F\left(X\right)”⟩$$
Assertion	cats1co	$$⊢\phi \to F\circ T=V$$

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	$$⊢T=S\mathrm{++}⟨“X”⟩$$
2		cats1cld.2	$$⊢\phi \to S\in \mathrm{Word}A$$
3		cats1cld.3	$$⊢\phi \to X\in A$$
4		cats1co.4	$$⊢\phi \to F:A⟶B$$
5		cats1co.5	$$⊢\phi \to F\circ S=U$$
6		cats1co.6	$$⊢V=U\mathrm{++}⟨“F\left(X\right)”⟩$$
7	3	s1cld	$$⊢\phi \to ⟨“X”⟩\in \mathrm{Word}A$$
8		ccatco	$$⊢\left(S\in \mathrm{Word}A\wedge ⟨“X”⟩\in \mathrm{Word}A\wedge F:A⟶B\right)\to F\circ \left(S\mathrm{++}⟨“X”⟩\right)=\left(F\circ S\right)\mathrm{++}\left(F\circ ⟨“X”⟩\right)$$
9	2 7 4 8	syl3anc	$$⊢\phi \to F\circ \left(S\mathrm{++}⟨“X”⟩\right)=\left(F\circ S\right)\mathrm{++}\left(F\circ ⟨“X”⟩\right)$$
10		s1co	$$⊢\left(X\in A\wedge F:A⟶B\right)\to F\circ ⟨“X”⟩=⟨“F\left(X\right)”⟩$$
11	3 4 10	syl2anc	$$⊢\phi \to F\circ ⟨“X”⟩=⟨“F\left(X\right)”⟩$$
12	5 11	oveq12d	$$⊢\phi \to \left(F\circ S\right)\mathrm{++}\left(F\circ ⟨“X”⟩\right)=U\mathrm{++}⟨“F\left(X\right)”⟩$$
13	9 12	eqtrd	$$⊢\phi \to F\circ \left(S\mathrm{++}⟨“X”⟩\right)=U\mathrm{++}⟨“F\left(X\right)”⟩$$
14	1	coeq2i	$$⊢F\circ T=F\circ \left(S\mathrm{++}⟨“X”⟩\right)$$
15	13 14 6	3eqtr4g	$$⊢\phi \to F\circ T=V$$