# Metamath Proof Explorer

## Theorem swrdccatin1

Description: The subword of a concatenation of two words within the first of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018)

Ref Expression
Assertion swrdccatin1 ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to \left(\left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩={A}\mathrm{substr}⟨{M},{N}⟩\right)$

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}\left|{A}\right|=0\to \left(0\dots \left|{A}\right|\right)=\left(0\dots 0\right)$
2 1 eleq2d ${⊢}\left|{A}\right|=0\to \left({N}\in \left(0\dots \left|{A}\right|\right)↔{N}\in \left(0\dots 0\right)\right)$
3 elfz1eq ${⊢}{N}\in \left(0\dots 0\right)\to {N}=0$
4 elfz1eq ${⊢}{M}\in \left(0\dots 0\right)\to {M}=0$
5 swrd00 ${⊢}\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨0,0⟩=\varnothing$
6 swrd00 ${⊢}{A}\mathrm{substr}⟨0,0⟩=\varnothing$
7 5 6 eqtr4i ${⊢}\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨0,0⟩={A}\mathrm{substr}⟨0,0⟩$
8 opeq1 ${⊢}{M}=0\to ⟨{M},0⟩=⟨0,0⟩$
9 8 oveq2d ${⊢}{M}=0\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},0⟩=\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨0,0⟩$
10 8 oveq2d ${⊢}{M}=0\to {A}\mathrm{substr}⟨{M},0⟩={A}\mathrm{substr}⟨0,0⟩$
11 7 9 10 3eqtr4a ${⊢}{M}=0\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},0⟩={A}\mathrm{substr}⟨{M},0⟩$
12 4 11 syl ${⊢}{M}\in \left(0\dots 0\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},0⟩={A}\mathrm{substr}⟨{M},0⟩$
13 oveq2 ${⊢}{N}=0\to \left(0\dots {N}\right)=\left(0\dots 0\right)$
14 13 eleq2d ${⊢}{N}=0\to \left({M}\in \left(0\dots {N}\right)↔{M}\in \left(0\dots 0\right)\right)$
15 opeq2 ${⊢}{N}=0\to ⟨{M},{N}⟩=⟨{M},0⟩$
16 15 oveq2d ${⊢}{N}=0\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩=\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},0⟩$
17 15 oveq2d ${⊢}{N}=0\to {A}\mathrm{substr}⟨{M},{N}⟩={A}\mathrm{substr}⟨{M},0⟩$
18 16 17 eqeq12d ${⊢}{N}=0\to \left(\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩={A}\mathrm{substr}⟨{M},{N}⟩↔\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},0⟩={A}\mathrm{substr}⟨{M},0⟩\right)$
19 14 18 imbi12d ${⊢}{N}=0\to \left(\left({M}\in \left(0\dots {N}\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩={A}\mathrm{substr}⟨{M},{N}⟩\right)↔\left({M}\in \left(0\dots 0\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},0⟩={A}\mathrm{substr}⟨{M},0⟩\right)\right)$
20 12 19 mpbiri ${⊢}{N}=0\to \left({M}\in \left(0\dots {N}\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩={A}\mathrm{substr}⟨{M},{N}⟩\right)$
21 3 20 syl ${⊢}{N}\in \left(0\dots 0\right)\to \left({M}\in \left(0\dots {N}\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩={A}\mathrm{substr}⟨{M},{N}⟩\right)$
22 2 21 syl6bi ${⊢}\left|{A}\right|=0\to \left({N}\in \left(0\dots \left|{A}\right|\right)\to \left({M}\in \left(0\dots {N}\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩={A}\mathrm{substr}⟨{M},{N}⟩\right)\right)$
23 22 impcomd ${⊢}\left|{A}\right|=0\to \left(\left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩={A}\mathrm{substr}⟨{M},{N}⟩\right)$
24 23 adantl ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|=0\right)\to \left(\left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩={A}\mathrm{substr}⟨{M},{N}⟩\right)$
25 ccatcl ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to {A}\mathrm{++}{B}\in \mathrm{Word}{V}$
26 25 ad2antrr ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\to {A}\mathrm{++}{B}\in \mathrm{Word}{V}$
27 simprl ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\to {M}\in \left(0\dots {N}\right)$
28 elfzelfzccat ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to \left({N}\in \left(0\dots \left|{A}\right|\right)\to {N}\in \left(0\dots \left|{A}\mathrm{++}{B}\right|\right)\right)$
29 28 imp ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\to {N}\in \left(0\dots \left|{A}\mathrm{++}{B}\right|\right)$
30 29 ad2ant2rl ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\to {N}\in \left(0\dots \left|{A}\mathrm{++}{B}\right|\right)$
31 swrdvalfn ${⊢}\left({A}\mathrm{++}{B}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\mathrm{++}{B}\right|\right)\right)\to \left(\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩\right)Fn\left(0..^{N}-{M}\right)$
32 26 27 30 31 syl3anc ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\to \left(\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩\right)Fn\left(0..^{N}-{M}\right)$
33 3anass ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)↔\left({A}\in \mathrm{Word}{V}\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)$
34 33 simplbi2 ${⊢}{A}\in \mathrm{Word}{V}\to \left(\left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\to \left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)$
35 34 ad2antrr ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\to \left(\left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\to \left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)$
36 35 imp ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\to \left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)$
37 swrdvalfn ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\to \left({A}\mathrm{substr}⟨{M},{N}⟩\right)Fn\left(0..^{N}-{M}\right)$
38 36 37 syl ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\to \left({A}\mathrm{substr}⟨{M},{N}⟩\right)Fn\left(0..^{N}-{M}\right)$
39 simp-4l ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to {A}\in \mathrm{Word}{V}$
40 simp-4r ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to {B}\in \mathrm{Word}{V}$
41 elfznn0 ${⊢}{M}\in \left(0\dots {N}\right)\to {M}\in {ℕ}_{0}$
42 nn0addcl ${⊢}\left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to {k}+{M}\in {ℕ}_{0}$
43 42 expcom ${⊢}{M}\in {ℕ}_{0}\to \left({k}\in {ℕ}_{0}\to {k}+{M}\in {ℕ}_{0}\right)$
44 41 43 syl ${⊢}{M}\in \left(0\dots {N}\right)\to \left({k}\in {ℕ}_{0}\to {k}+{M}\in {ℕ}_{0}\right)$
45 44 ad2antrl ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\to \left({k}\in {ℕ}_{0}\to {k}+{M}\in {ℕ}_{0}\right)$
46 elfzonn0 ${⊢}{k}\in \left(0..^{N}-{M}\right)\to {k}\in {ℕ}_{0}$
47 45 46 impel ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to {k}+{M}\in {ℕ}_{0}$
48 lencl ${⊢}{A}\in \mathrm{Word}{V}\to \left|{A}\right|\in {ℕ}_{0}$
49 elnnne0 ${⊢}\left|{A}\right|\in ℕ↔\left(\left|{A}\right|\in {ℕ}_{0}\wedge \left|{A}\right|\ne 0\right)$
50 49 simplbi2 ${⊢}\left|{A}\right|\in {ℕ}_{0}\to \left(\left|{A}\right|\ne 0\to \left|{A}\right|\in ℕ\right)$
51 48 50 syl ${⊢}{A}\in \mathrm{Word}{V}\to \left(\left|{A}\right|\ne 0\to \left|{A}\right|\in ℕ\right)$
52 51 adantr ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to \left(\left|{A}\right|\ne 0\to \left|{A}\right|\in ℕ\right)$
53 52 imp ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\to \left|{A}\right|\in ℕ$
54 53 ad2antrr ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to \left|{A}\right|\in ℕ$
55 elfzo0 ${⊢}{k}\in \left(0..^{N}-{M}\right)↔\left({k}\in {ℕ}_{0}\wedge {N}-{M}\in ℕ\wedge {k}<{N}-{M}\right)$
56 elfz2nn0 ${⊢}{N}\in \left(0\dots \left|{A}\right|\right)↔\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\wedge {N}\le \left|{A}\right|\right)$
57 nn0re ${⊢}{k}\in {ℕ}_{0}\to {k}\in ℝ$
58 57 ad2antrl ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\right)\wedge \left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\right)\to {k}\in ℝ$
59 nn0re ${⊢}{M}\in {ℕ}_{0}\to {M}\in ℝ$
60 59 ad2antll ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\right)\wedge \left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\right)\to {M}\in ℝ$
61 nn0re ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℝ$
62 61 ad2antrr ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\right)\wedge \left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\right)\to {N}\in ℝ$
63 58 60 62 ltaddsubd ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\right)\wedge \left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\right)\to \left({k}+{M}<{N}↔{k}<{N}-{M}\right)$
64 nn0readdcl ${⊢}\left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to {k}+{M}\in ℝ$
65 64 adantl ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\right)\wedge \left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\right)\to {k}+{M}\in ℝ$
66 nn0re ${⊢}\left|{A}\right|\in {ℕ}_{0}\to \left|{A}\right|\in ℝ$
67 66 ad2antlr ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\right)\wedge \left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\right)\to \left|{A}\right|\in ℝ$
68 ltletr ${⊢}\left({k}+{M}\in ℝ\wedge {N}\in ℝ\wedge \left|{A}\right|\in ℝ\right)\to \left(\left({k}+{M}<{N}\wedge {N}\le \left|{A}\right|\right)\to {k}+{M}<\left|{A}\right|\right)$
69 65 62 67 68 syl3anc ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\right)\wedge \left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\right)\to \left(\left({k}+{M}<{N}\wedge {N}\le \left|{A}\right|\right)\to {k}+{M}<\left|{A}\right|\right)$
70 69 expd ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\right)\wedge \left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\right)\to \left({k}+{M}<{N}\to \left({N}\le \left|{A}\right|\to {k}+{M}<\left|{A}\right|\right)\right)$
71 63 70 sylbird ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\right)\wedge \left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\right)\to \left({k}<{N}-{M}\to \left({N}\le \left|{A}\right|\to {k}+{M}<\left|{A}\right|\right)\right)$
72 71 ex ${⊢}\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\right)\to \left(\left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to \left({k}<{N}-{M}\to \left({N}\le \left|{A}\right|\to {k}+{M}<\left|{A}\right|\right)\right)\right)$
73 72 com24 ${⊢}\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\right)\to \left({N}\le \left|{A}\right|\to \left({k}<{N}-{M}\to \left(\left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to {k}+{M}<\left|{A}\right|\right)\right)\right)$
74 73 3impia ${⊢}\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\wedge {N}\le \left|{A}\right|\right)\to \left({k}<{N}-{M}\to \left(\left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to {k}+{M}<\left|{A}\right|\right)\right)$
75 74 com13 ${⊢}\left({k}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to \left({k}<{N}-{M}\to \left(\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\wedge {N}\le \left|{A}\right|\right)\to {k}+{M}<\left|{A}\right|\right)\right)$
76 75 impancom ${⊢}\left({k}\in {ℕ}_{0}\wedge {k}<{N}-{M}\right)\to \left({M}\in {ℕ}_{0}\to \left(\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\wedge {N}\le \left|{A}\right|\right)\to {k}+{M}<\left|{A}\right|\right)\right)$
77 76 3adant2 ${⊢}\left({k}\in {ℕ}_{0}\wedge {N}-{M}\in ℕ\wedge {k}<{N}-{M}\right)\to \left({M}\in {ℕ}_{0}\to \left(\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\wedge {N}\le \left|{A}\right|\right)\to {k}+{M}<\left|{A}\right|\right)\right)$
78 77 com13 ${⊢}\left({N}\in {ℕ}_{0}\wedge \left|{A}\right|\in {ℕ}_{0}\wedge {N}\le \left|{A}\right|\right)\to \left({M}\in {ℕ}_{0}\to \left(\left({k}\in {ℕ}_{0}\wedge {N}-{M}\in ℕ\wedge {k}<{N}-{M}\right)\to {k}+{M}<\left|{A}\right|\right)\right)$
79 56 78 sylbi ${⊢}{N}\in \left(0\dots \left|{A}\right|\right)\to \left({M}\in {ℕ}_{0}\to \left(\left({k}\in {ℕ}_{0}\wedge {N}-{M}\in ℕ\wedge {k}<{N}-{M}\right)\to {k}+{M}<\left|{A}\right|\right)\right)$
80 41 79 mpan9 ${⊢}\left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {ℕ}_{0}\wedge {N}-{M}\in ℕ\wedge {k}<{N}-{M}\right)\to {k}+{M}<\left|{A}\right|\right)$
81 80 adantl ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\to \left(\left({k}\in {ℕ}_{0}\wedge {N}-{M}\in ℕ\wedge {k}<{N}-{M}\right)\to {k}+{M}<\left|{A}\right|\right)$
82 55 81 syl5bi ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\to \left({k}\in \left(0..^{N}-{M}\right)\to {k}+{M}<\left|{A}\right|\right)$
83 82 imp ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to {k}+{M}<\left|{A}\right|$
84 elfzo0 ${⊢}{k}+{M}\in \left(0..^\left|{A}\right|\right)↔\left({k}+{M}\in {ℕ}_{0}\wedge \left|{A}\right|\in ℕ\wedge {k}+{M}<\left|{A}\right|\right)$
85 47 54 83 84 syl3anbrc ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to {k}+{M}\in \left(0..^\left|{A}\right|\right)$
86 ccatval1 ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\wedge {k}+{M}\in \left(0..^\left|{A}\right|\right)\right)\to \left({A}\mathrm{++}{B}\right)\left({k}+{M}\right)={A}\left({k}+{M}\right)$
87 39 40 85 86 syl3anc ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to \left({A}\mathrm{++}{B}\right)\left({k}+{M}\right)={A}\left({k}+{M}\right)$
88 25 ad5ant12 ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to {A}\mathrm{++}{B}\in \mathrm{Word}{V}$
89 simplrl ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to {M}\in \left(0\dots {N}\right)$
90 30 adantr ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to {N}\in \left(0\dots \left|{A}\mathrm{++}{B}\right|\right)$
91 simpr ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to {k}\in \left(0..^{N}-{M}\right)$
92 swrdfv ${⊢}\left(\left({A}\mathrm{++}{B}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\mathrm{++}{B}\right|\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to \left(\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩\right)\left({k}\right)=\left({A}\mathrm{++}{B}\right)\left({k}+{M}\right)$
93 88 89 90 91 92 syl31anc ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to \left(\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩\right)\left({k}\right)=\left({A}\mathrm{++}{B}\right)\left({k}+{M}\right)$
94 swrdfv ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to \left({A}\mathrm{substr}⟨{M},{N}⟩\right)\left({k}\right)={A}\left({k}+{M}\right)$
95 36 94 sylan ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to \left({A}\mathrm{substr}⟨{M},{N}⟩\right)\left({k}\right)={A}\left({k}+{M}\right)$
96 87 93 95 3eqtr4d ${⊢}\left(\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\wedge {k}\in \left(0..^{N}-{M}\right)\right)\to \left(\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩\right)\left({k}\right)=\left({A}\mathrm{substr}⟨{M},{N}⟩\right)\left({k}\right)$
97 32 38 96 eqfnfvd ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\wedge \left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩={A}\mathrm{substr}⟨{M},{N}⟩$
98 97 ex ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{A}\right|\ne 0\right)\to \left(\left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩={A}\mathrm{substr}⟨{M},{N}⟩\right)$
99 24 98 pm2.61dane ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to \left(\left({M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\right|\right)\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩={A}\mathrm{substr}⟨{M},{N}⟩\right)$