Theorem cats1fv

Description: A symbol other than the last in 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$$
	cats1fv.4	$$⊢Y\in V\to S\left(N\right)=Y$$
	cats1fv.5	$$⊢N\in {\mathbb{N}}_0$$
	cats1fv.6	$$⊢N<M$$
Assertion	cats1fv	$$⊢Y\in V\to T\left(N\right)=Y$$

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		cats1fv.4	$$⊢Y\in V\to S\left(N\right)=Y$$
5		cats1fv.5	$$⊢N\in {\mathbb{N}}_0$$
6		cats1fv.6	$$⊢N<M$$
7	1	fveq1i	$$⊢T\left(N\right)=\left(S\mathrm{++}⟨“X”⟩\right)\left(N\right)$$
8		s1cli	$$⊢⟨“X”⟩\in \mathrm{Word}\mathrm{V}$$
9		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
10	5 9	eleqtri	$$⊢N\in {\mathbb{Z}}_{\ge 0}$$
11		lencl	$$⊢S\in \mathrm{Word}\mathrm{V}\to \left|S\right|\in {\mathbb{N}}_0$$
12		nn0z	$$⊢\left|S\right|\in {\mathbb{N}}_0\to \left|S\right|\in \mathbb{Z}$$
13	2 11 12	mp2b	$$⊢\left|S\right|\in \mathbb{Z}$$
14	6 3	breqtrri	$$⊢N<\left|S\right|$$
15		elfzo2	$$⊢N\in \left(0..^\left|S\right|\right)\leftrightarrow \left(N\in {\mathbb{Z}}_{\ge 0}\wedge \left|S\right|\in \mathbb{Z}\wedge N<\left|S\right|\right)$$
16	10 13 14 15	mpbir3an	$$⊢N\in \left(0..^\left|S\right|\right)$$
17		ccatval1	$$⊢\left(S\in \mathrm{Word}\mathrm{V}\wedge ⟨“X”⟩\in \mathrm{Word}\mathrm{V}\wedge N\in \left(0..^\left|S\right|\right)\right)\to \left(S\mathrm{++}⟨“X”⟩\right)\left(N\right)=S\left(N\right)$$
18	2 8 16 17	mp3an	$$⊢\left(S\mathrm{++}⟨“X”⟩\right)\left(N\right)=S\left(N\right)$$
19	7 18	eqtri	$$⊢T\left(N\right)=S\left(N\right)$$
20	19 4	syl5eq	$$⊢Y\in V\to T\left(N\right)=Y$$