# Metamath Proof Explorer

## 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 {ℕ}_{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 {ℕ}_{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 ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
10 5 9 eleqtri ${⊢}{N}\in {ℤ}_{\ge 0}$
11 lencl ${⊢}{S}\in \mathrm{Word}\mathrm{V}\to \left|{S}\right|\in {ℕ}_{0}$
12 nn0z ${⊢}\left|{S}\right|\in {ℕ}_{0}\to \left|{S}\right|\in ℤ$
13 2 11 12 mp2b ${⊢}\left|{S}\right|\in ℤ$
14 6 3 breqtrri ${⊢}{N}<\left|{S}\right|$
15 elfzo2 ${⊢}{N}\in \left(0..^\left|{S}\right|\right)↔\left({N}\in {ℤ}_{\ge 0}\wedge \left|{S}\right|\in ℤ\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}$