Theorem cats1len

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

	Ref	Expression
Hypotheses	cats1cld.1	$$⊢T=S\mathrm{++}⟨“X”⟩$$
	cats1cli.2	$$⊢S\in \mathrm{Word}\mathrm{V}$$
	cats1fvn.3	$$⊢\left|S\right|=M$$
	cats1len.4	$$⊢M+1=N$$
Assertion	cats1len	$$⊢\left|T\right|=N$$

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	$$⊢T=S\mathrm{++}⟨“X”⟩$$
2		cats1cli.2	$$⊢S\in \mathrm{Word}\mathrm{V}$$
3		cats1fvn.3	$$⊢\left|S\right|=M$$
4		cats1len.4	$$⊢M+1=N$$
5	1	fveq2i	$$⊢\left|T\right|=\left|S\mathrm{++}⟨“X”⟩\right|$$
6		s1cli	$$⊢⟨“X”⟩\in \mathrm{Word}\mathrm{V}$$
7		ccatlen	$$⊢\left(S\in \mathrm{Word}\mathrm{V}\wedge ⟨“X”⟩\in \mathrm{Word}\mathrm{V}\right)\to \left|S\mathrm{++}⟨“X”⟩\right|=\left|S\right|+\left|⟨“X”⟩\right|$$
8	2 6 7	mp2an	$$⊢\left|S\mathrm{++}⟨“X”⟩\right|=\left|S\right|+\left|⟨“X”⟩\right|$$
9		s1len	$$⊢\left|⟨“X”⟩\right|=1$$
10	3 9	oveq12i	$$⊢\left|S\right|+\left|⟨“X”⟩\right|=M+1$$
11	8 10	eqtri	$$⊢\left|S\mathrm{++}⟨“X”⟩\right|=M+1$$
12	11 4	eqtri	$$⊢\left|S\mathrm{++}⟨“X”⟩\right|=N$$
13	5 12	eqtri	$$⊢\left|T\right|=N$$