Theorem cats1fvn

Description: The last symbol of a 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$$
Assertion	cats1fvn	$$⊢X\in V\to T\left(M\right)=X$$

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	3	oveq2i	$$⊢0+\left|S\right|=0+M$$
5		lencl	$$⊢S\in \mathrm{Word}\mathrm{V}\to \left|S\right|\in {\mathbb{N}}_0$$
6	2 5	ax-mp	$$⊢\left|S\right|\in {\mathbb{N}}_0$$
7	3 6	eqeltrri	$$⊢M\in {\mathbb{N}}_0$$
8	7	nn0cni	$$⊢M\in ℂ$$
9	8	addid2i	$$⊢0+M=M$$
10	4 9	eqtr2i	$$⊢M=0+\left|S\right|$$
11	1 10	fveq12i	$$⊢T\left(M\right)=\left(S\mathrm{++}⟨“X”⟩\right)\left(0+\left|S\right|\right)$$
12		s1cli	$$⊢⟨“X”⟩\in \mathrm{Word}\mathrm{V}$$
13		s1len	$$⊢\left|⟨“X”⟩\right|=1$$
14		1nn	$$⊢1\in \mathbb{N}$$
15	13 14	eqeltri	$$⊢\left|⟨“X”⟩\right|\in \mathbb{N}$$
16		lbfzo0	$$⊢0\in \left(0..^\left|⟨“X”⟩\right|\right)\leftrightarrow \left|⟨“X”⟩\right|\in \mathbb{N}$$
17	15 16	mpbir	$$⊢0\in \left(0..^\left|⟨“X”⟩\right|\right)$$
18		ccatval3	$$⊢\left(S\in \mathrm{Word}\mathrm{V}\wedge ⟨“X”⟩\in \mathrm{Word}\mathrm{V}\wedge 0\in \left(0..^\left|⟨“X”⟩\right|\right)\right)\to \left(S\mathrm{++}⟨“X”⟩\right)\left(0+\left|S\right|\right)=⟨“X”⟩\left(0\right)$$
19	2 12 17 18	mp3an	$$⊢\left(S\mathrm{++}⟨“X”⟩\right)\left(0+\left|S\right|\right)=⟨“X”⟩\left(0\right)$$
20	11 19	eqtri	$$⊢T\left(M\right)=⟨“X”⟩\left(0\right)$$
21		s1fv	$$⊢X\in V\to ⟨“X”⟩\left(0\right)=X$$
22	20 21	syl5eq	$$⊢X\in V\to T\left(M\right)=X$$