Metamath Proof Explorer

Theorem ccatpfx

Description: Concatenating a prefix with an adjacent subword makes a longer prefix. (Contributed by AV, 7-May-2020)

Ref Expression
Assertion ccatpfx ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\to \left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)={S}\mathrm{prefix}{Z}$

Proof

Step Hyp Ref Expression
1 pfxcl ${⊢}{S}\in \mathrm{Word}{A}\to {S}\mathrm{prefix}{Y}\in \mathrm{Word}{A}$
2 swrdcl ${⊢}{S}\in \mathrm{Word}{A}\to {S}\mathrm{substr}⟨{Y},{Z}⟩\in \mathrm{Word}{A}$
3 ccatcl ${⊢}\left({S}\mathrm{prefix}{Y}\in \mathrm{Word}{A}\wedge {S}\mathrm{substr}⟨{Y},{Z}⟩\in \mathrm{Word}{A}\right)\to \left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\in \mathrm{Word}{A}$
4 1 2 3 syl2anc ${⊢}{S}\in \mathrm{Word}{A}\to \left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\in \mathrm{Word}{A}$
5 wrdfn ${⊢}\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\in \mathrm{Word}{A}\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)Fn\left(0..^\left|\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right|\right)$
6 4 5 syl ${⊢}{S}\in \mathrm{Word}{A}\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)Fn\left(0..^\left|\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right|\right)$
7 6 adantr ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)Fn\left(0..^\left|\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right|\right)$
8 ccatlen ${⊢}\left({S}\mathrm{prefix}{Y}\in \mathrm{Word}{A}\wedge {S}\mathrm{substr}⟨{Y},{Z}⟩\in \mathrm{Word}{A}\right)\to \left|\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right|=\left|{S}\mathrm{prefix}{Y}\right|+\left|{S}\mathrm{substr}⟨{Y},{Z}⟩\right|$
9 1 2 8 syl2anc ${⊢}{S}\in \mathrm{Word}{A}\to \left|\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right|=\left|{S}\mathrm{prefix}{Y}\right|+\left|{S}\mathrm{substr}⟨{Y},{Z}⟩\right|$
10 9 adantr ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left|\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right|=\left|{S}\mathrm{prefix}{Y}\right|+\left|{S}\mathrm{substr}⟨{Y},{Z}⟩\right|$
11 fzass4 ${⊢}\left({Y}\in \left(0\dots \left|{S}\right|\right)\wedge {Z}\in \left({Y}\dots \left|{S}\right|\right)\right)↔\left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)$
12 11 biimpri ${⊢}\left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\to \left({Y}\in \left(0\dots \left|{S}\right|\right)\wedge {Z}\in \left({Y}\dots \left|{S}\right|\right)\right)$
13 12 simpld ${⊢}\left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\to {Y}\in \left(0\dots \left|{S}\right|\right)$
14 pfxlen ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {Y}\in \left(0\dots \left|{S}\right|\right)\right)\to \left|{S}\mathrm{prefix}{Y}\right|={Y}$
15 13 14 sylan2 ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left|{S}\mathrm{prefix}{Y}\right|={Y}$
16 swrdlen ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\to \left|{S}\mathrm{substr}⟨{Y},{Z}⟩\right|={Z}-{Y}$
17 16 3expb ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left|{S}\mathrm{substr}⟨{Y},{Z}⟩\right|={Z}-{Y}$
18 15 17 oveq12d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left|{S}\mathrm{prefix}{Y}\right|+\left|{S}\mathrm{substr}⟨{Y},{Z}⟩\right|={Y}+{Z}-{Y}$
19 elfzelz ${⊢}{Y}\in \left(0\dots {Z}\right)\to {Y}\in ℤ$
20 19 zcnd ${⊢}{Y}\in \left(0\dots {Z}\right)\to {Y}\in ℂ$
21 elfzelz ${⊢}{Z}\in \left(0\dots \left|{S}\right|\right)\to {Z}\in ℤ$
22 21 zcnd ${⊢}{Z}\in \left(0\dots \left|{S}\right|\right)\to {Z}\in ℂ$
23 pncan3 ${⊢}\left({Y}\in ℂ\wedge {Z}\in ℂ\right)\to {Y}+{Z}-{Y}={Z}$
24 20 22 23 syl2an ${⊢}\left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\to {Y}+{Z}-{Y}={Z}$
25 24 adantl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to {Y}+{Z}-{Y}={Z}$
26 10 18 25 3eqtrd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left|\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right|={Z}$
27 26 oveq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left(0..^\left|\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right|\right)=\left(0..^{Z}\right)$
28 27 fneq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left(\left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)Fn\left(0..^\left|\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right|\right)↔\left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)Fn\left(0..^{Z}\right)\right)$
29 7 28 mpbid ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)Fn\left(0..^{Z}\right)$
30 pfxfn ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\to \left({S}\mathrm{prefix}{Z}\right)Fn\left(0..^{Z}\right)$
31 30 adantrl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left({S}\mathrm{prefix}{Z}\right)Fn\left(0..^{Z}\right)$
32 id ${⊢}{x}\in \left(0..^{Z}\right)\to {x}\in \left(0..^{Z}\right)$
33 19 ad2antrl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to {Y}\in ℤ$
34 fzospliti ${⊢}\left({x}\in \left(0..^{Z}\right)\wedge {Y}\in ℤ\right)\to \left({x}\in \left(0..^{Y}\right)\vee {x}\in \left({Y}..^{Z}\right)\right)$
35 32 33 34 syl2anr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left(0..^{Z}\right)\right)\to \left({x}\in \left(0..^{Y}\right)\vee {x}\in \left({Y}..^{Z}\right)\right)$
36 1 ad2antrr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left(0..^{Y}\right)\right)\to {S}\mathrm{prefix}{Y}\in \mathrm{Word}{A}$
37 2 ad2antrr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left(0..^{Y}\right)\right)\to {S}\mathrm{substr}⟨{Y},{Z}⟩\in \mathrm{Word}{A}$
38 15 oveq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left(0..^\left|{S}\mathrm{prefix}{Y}\right|\right)=\left(0..^{Y}\right)$
39 38 eleq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left({x}\in \left(0..^\left|{S}\mathrm{prefix}{Y}\right|\right)↔{x}\in \left(0..^{Y}\right)\right)$
40 39 biimpar ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left(0..^{Y}\right)\right)\to {x}\in \left(0..^\left|{S}\mathrm{prefix}{Y}\right|\right)$
41 ccatval1 ${⊢}\left({S}\mathrm{prefix}{Y}\in \mathrm{Word}{A}\wedge {S}\mathrm{substr}⟨{Y},{Z}⟩\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{S}\mathrm{prefix}{Y}\right|\right)\right)\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)\left({x}\right)=\left({S}\mathrm{prefix}{Y}\right)\left({x}\right)$
42 36 37 40 41 syl3anc ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left(0..^{Y}\right)\right)\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)\left({x}\right)=\left({S}\mathrm{prefix}{Y}\right)\left({x}\right)$
43 simpl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to {S}\in \mathrm{Word}{A}$
44 13 adantl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to {Y}\in \left(0\dots \left|{S}\right|\right)$
45 id ${⊢}{x}\in \left(0..^{Y}\right)\to {x}\in \left(0..^{Y}\right)$
46 pfxfv ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {Y}\in \left(0\dots \left|{S}\right|\right)\wedge {x}\in \left(0..^{Y}\right)\right)\to \left({S}\mathrm{prefix}{Y}\right)\left({x}\right)={S}\left({x}\right)$
47 43 44 45 46 syl2an3an ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left(0..^{Y}\right)\right)\to \left({S}\mathrm{prefix}{Y}\right)\left({x}\right)={S}\left({x}\right)$
48 42 47 eqtrd ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left(0..^{Y}\right)\right)\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)\left({x}\right)={S}\left({x}\right)$
49 1 ad2antrr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to {S}\mathrm{prefix}{Y}\in \mathrm{Word}{A}$
50 2 ad2antrr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to {S}\mathrm{substr}⟨{Y},{Z}⟩\in \mathrm{Word}{A}$
51 18 25 eqtrd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left|{S}\mathrm{prefix}{Y}\right|+\left|{S}\mathrm{substr}⟨{Y},{Z}⟩\right|={Z}$
52 15 51 oveq12d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left(\left|{S}\mathrm{prefix}{Y}\right|..^\left|{S}\mathrm{prefix}{Y}\right|+\left|{S}\mathrm{substr}⟨{Y},{Z}⟩\right|\right)=\left({Y}..^{Z}\right)$
53 52 eleq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left({x}\in \left(\left|{S}\mathrm{prefix}{Y}\right|..^\left|{S}\mathrm{prefix}{Y}\right|+\left|{S}\mathrm{substr}⟨{Y},{Z}⟩\right|\right)↔{x}\in \left({Y}..^{Z}\right)\right)$
54 53 biimpar ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to {x}\in \left(\left|{S}\mathrm{prefix}{Y}\right|..^\left|{S}\mathrm{prefix}{Y}\right|+\left|{S}\mathrm{substr}⟨{Y},{Z}⟩\right|\right)$
55 ccatval2 ${⊢}\left({S}\mathrm{prefix}{Y}\in \mathrm{Word}{A}\wedge {S}\mathrm{substr}⟨{Y},{Z}⟩\in \mathrm{Word}{A}\wedge {x}\in \left(\left|{S}\mathrm{prefix}{Y}\right|..^\left|{S}\mathrm{prefix}{Y}\right|+\left|{S}\mathrm{substr}⟨{Y},{Z}⟩\right|\right)\right)\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)\left({x}\right)=\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\left({x}-\left|{S}\mathrm{prefix}{Y}\right|\right)$
56 49 50 54 55 syl3anc ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)\left({x}\right)=\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\left({x}-\left|{S}\mathrm{prefix}{Y}\right|\right)$
57 id ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\to \left({S}\in \mathrm{Word}{A}\wedge {Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)$
58 57 3expb ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left({S}\in \mathrm{Word}{A}\wedge {Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)$
59 15 oveq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to {x}-\left|{S}\mathrm{prefix}{Y}\right|={x}-{Y}$
60 59 adantr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to {x}-\left|{S}\mathrm{prefix}{Y}\right|={x}-{Y}$
61 id ${⊢}{x}\in \left({Y}..^{Z}\right)\to {x}\in \left({Y}..^{Z}\right)$
62 fzosubel ${⊢}\left({x}\in \left({Y}..^{Z}\right)\wedge {Y}\in ℤ\right)\to {x}-{Y}\in \left({Y}-{Y}..^{Z}-{Y}\right)$
63 61 33 62 syl2anr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to {x}-{Y}\in \left({Y}-{Y}..^{Z}-{Y}\right)$
64 20 subidd ${⊢}{Y}\in \left(0\dots {Z}\right)\to {Y}-{Y}=0$
65 64 oveq1d ${⊢}{Y}\in \left(0\dots {Z}\right)\to \left({Y}-{Y}..^{Z}-{Y}\right)=\left(0..^{Z}-{Y}\right)$
66 65 eleq2d ${⊢}{Y}\in \left(0\dots {Z}\right)\to \left({x}-{Y}\in \left({Y}-{Y}..^{Z}-{Y}\right)↔{x}-{Y}\in \left(0..^{Z}-{Y}\right)\right)$
67 66 ad2antrl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left({x}-{Y}\in \left({Y}-{Y}..^{Z}-{Y}\right)↔{x}-{Y}\in \left(0..^{Z}-{Y}\right)\right)$
68 67 adantr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to \left({x}-{Y}\in \left({Y}-{Y}..^{Z}-{Y}\right)↔{x}-{Y}\in \left(0..^{Z}-{Y}\right)\right)$
69 63 68 mpbid ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to {x}-{Y}\in \left(0..^{Z}-{Y}\right)$
70 60 69 eqeltrd ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to {x}-\left|{S}\mathrm{prefix}{Y}\right|\in \left(0..^{Z}-{Y}\right)$
71 swrdfv ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\wedge {x}-\left|{S}\mathrm{prefix}{Y}\right|\in \left(0..^{Z}-{Y}\right)\right)\to \left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\left({x}-\left|{S}\mathrm{prefix}{Y}\right|\right)={S}\left({x}-\left|{S}\mathrm{prefix}{Y}\right|+{Y}\right)$
72 58 70 71 syl2an2r ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to \left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\left({x}-\left|{S}\mathrm{prefix}{Y}\right|\right)={S}\left({x}-\left|{S}\mathrm{prefix}{Y}\right|+{Y}\right)$
73 59 oveq1d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to {x}-\left|{S}\mathrm{prefix}{Y}\right|+{Y}={x}-{Y}+{Y}$
74 73 adantr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to {x}-\left|{S}\mathrm{prefix}{Y}\right|+{Y}={x}-{Y}+{Y}$
75 elfzoelz ${⊢}{x}\in \left({Y}..^{Z}\right)\to {x}\in ℤ$
76 75 zcnd ${⊢}{x}\in \left({Y}..^{Z}\right)\to {x}\in ℂ$
77 20 ad2antrl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to {Y}\in ℂ$
78 npcan ${⊢}\left({x}\in ℂ\wedge {Y}\in ℂ\right)\to {x}-{Y}+{Y}={x}$
79 76 77 78 syl2anr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to {x}-{Y}+{Y}={x}$
80 74 79 eqtrd ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to {x}-\left|{S}\mathrm{prefix}{Y}\right|+{Y}={x}$
81 80 fveq2d ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to {S}\left({x}-\left|{S}\mathrm{prefix}{Y}\right|+{Y}\right)={S}\left({x}\right)$
82 56 72 81 3eqtrd ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left({Y}..^{Z}\right)\right)\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)\left({x}\right)={S}\left({x}\right)$
83 48 82 jaodan ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge \left({x}\in \left(0..^{Y}\right)\vee {x}\in \left({Y}..^{Z}\right)\right)\right)\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)\left({x}\right)={S}\left({x}\right)$
84 35 83 syldan ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left(0..^{Z}\right)\right)\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)\left({x}\right)={S}\left({x}\right)$
85 pfxfv ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\wedge {x}\in \left(0..^{Z}\right)\right)\to \left({S}\mathrm{prefix}{Z}\right)\left({x}\right)={S}\left({x}\right)$
86 85 3expa ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\wedge {x}\in \left(0..^{Z}\right)\right)\to \left({S}\mathrm{prefix}{Z}\right)\left({x}\right)={S}\left({x}\right)$
87 86 adantlrl ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left(0..^{Z}\right)\right)\to \left({S}\mathrm{prefix}{Z}\right)\left({x}\right)={S}\left({x}\right)$
88 84 87 eqtr4d ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\wedge {x}\in \left(0..^{Z}\right)\right)\to \left(\left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)\right)\left({x}\right)=\left({S}\mathrm{prefix}{Z}\right)\left({x}\right)$
89 29 31 88 eqfnfvd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge \left({Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\right)\to \left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)={S}\mathrm{prefix}{Z}$
90 89 3impb ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {Y}\in \left(0\dots {Z}\right)\wedge {Z}\in \left(0\dots \left|{S}\right|\right)\right)\to \left({S}\mathrm{prefix}{Y}\right)\mathrm{++}\left({S}\mathrm{substr}⟨{Y},{Z}⟩\right)={S}\mathrm{prefix}{Z}$