# Metamath Proof Explorer

## Theorem swrdccat3blem

Description: Lemma for swrdccat3b . (Contributed by AV, 30-May-2018)

Ref Expression
Hypothesis swrdccatin2.l ${⊢}{L}=\left|{A}\right|$
Assertion swrdccat3blem ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge {M}\in \left(0\dots {L}+\left|{B}\right|\right)\right)\wedge {L}+\left|{B}\right|\le {L}\right)\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩$

### Proof

Step Hyp Ref Expression
1 swrdccatin2.l ${⊢}{L}=\left|{A}\right|$
2 lencl ${⊢}{B}\in \mathrm{Word}{V}\to \left|{B}\right|\in {ℕ}_{0}$
3 nn0le0eq0 ${⊢}\left|{B}\right|\in {ℕ}_{0}\to \left(\left|{B}\right|\le 0↔\left|{B}\right|=0\right)$
4 3 biimpd ${⊢}\left|{B}\right|\in {ℕ}_{0}\to \left(\left|{B}\right|\le 0\to \left|{B}\right|=0\right)$
5 2 4 syl ${⊢}{B}\in \mathrm{Word}{V}\to \left(\left|{B}\right|\le 0\to \left|{B}\right|=0\right)$
6 5 adantl ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to \left(\left|{B}\right|\le 0\to \left|{B}\right|=0\right)$
7 hasheq0 ${⊢}{B}\in \mathrm{Word}{V}\to \left(\left|{B}\right|=0↔{B}=\varnothing \right)$
8 7 biimpd ${⊢}{B}\in \mathrm{Word}{V}\to \left(\left|{B}\right|=0\to {B}=\varnothing \right)$
9 8 adantl ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to \left(\left|{B}\right|=0\to {B}=\varnothing \right)$
10 9 imp ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{B}\right|=0\right)\to {B}=\varnothing$
11 lencl ${⊢}{A}\in \mathrm{Word}{V}\to \left|{A}\right|\in {ℕ}_{0}$
12 1 eqcomi ${⊢}\left|{A}\right|={L}$
13 12 eleq1i ${⊢}\left|{A}\right|\in {ℕ}_{0}↔{L}\in {ℕ}_{0}$
14 nn0re ${⊢}{L}\in {ℕ}_{0}\to {L}\in ℝ$
15 elfz2nn0 ${⊢}{M}\in \left(0\dots {L}+0\right)↔\left({M}\in {ℕ}_{0}\wedge {L}+0\in {ℕ}_{0}\wedge {M}\le {L}+0\right)$
16 recn ${⊢}{L}\in ℝ\to {L}\in ℂ$
17 16 addid1d ${⊢}{L}\in ℝ\to {L}+0={L}$
18 17 breq2d ${⊢}{L}\in ℝ\to \left({M}\le {L}+0↔{M}\le {L}\right)$
19 nn0re ${⊢}{M}\in {ℕ}_{0}\to {M}\in ℝ$
20 19 anim1i ${⊢}\left({M}\in {ℕ}_{0}\wedge {L}\in ℝ\right)\to \left({M}\in ℝ\wedge {L}\in ℝ\right)$
21 20 ancoms ${⊢}\left({L}\in ℝ\wedge {M}\in {ℕ}_{0}\right)\to \left({M}\in ℝ\wedge {L}\in ℝ\right)$
22 letri3 ${⊢}\left({M}\in ℝ\wedge {L}\in ℝ\right)\to \left({M}={L}↔\left({M}\le {L}\wedge {L}\le {M}\right)\right)$
23 21 22 syl ${⊢}\left({L}\in ℝ\wedge {M}\in {ℕ}_{0}\right)\to \left({M}={L}↔\left({M}\le {L}\wedge {L}\le {M}\right)\right)$
24 23 biimprd ${⊢}\left({L}\in ℝ\wedge {M}\in {ℕ}_{0}\right)\to \left(\left({M}\le {L}\wedge {L}\le {M}\right)\to {M}={L}\right)$
25 24 exp4b ${⊢}{L}\in ℝ\to \left({M}\in {ℕ}_{0}\to \left({M}\le {L}\to \left({L}\le {M}\to {M}={L}\right)\right)\right)$
26 25 com23 ${⊢}{L}\in ℝ\to \left({M}\le {L}\to \left({M}\in {ℕ}_{0}\to \left({L}\le {M}\to {M}={L}\right)\right)\right)$
27 18 26 sylbid ${⊢}{L}\in ℝ\to \left({M}\le {L}+0\to \left({M}\in {ℕ}_{0}\to \left({L}\le {M}\to {M}={L}\right)\right)\right)$
28 27 com3l ${⊢}{M}\le {L}+0\to \left({M}\in {ℕ}_{0}\to \left({L}\in ℝ\to \left({L}\le {M}\to {M}={L}\right)\right)\right)$
29 28 impcom ${⊢}\left({M}\in {ℕ}_{0}\wedge {M}\le {L}+0\right)\to \left({L}\in ℝ\to \left({L}\le {M}\to {M}={L}\right)\right)$
30 29 3adant2 ${⊢}\left({M}\in {ℕ}_{0}\wedge {L}+0\in {ℕ}_{0}\wedge {M}\le {L}+0\right)\to \left({L}\in ℝ\to \left({L}\le {M}\to {M}={L}\right)\right)$
31 30 com12 ${⊢}{L}\in ℝ\to \left(\left({M}\in {ℕ}_{0}\wedge {L}+0\in {ℕ}_{0}\wedge {M}\le {L}+0\right)\to \left({L}\le {M}\to {M}={L}\right)\right)$
32 15 31 syl5bi ${⊢}{L}\in ℝ\to \left({M}\in \left(0\dots {L}+0\right)\to \left({L}\le {M}\to {M}={L}\right)\right)$
33 14 32 syl ${⊢}{L}\in {ℕ}_{0}\to \left({M}\in \left(0\dots {L}+0\right)\to \left({L}\le {M}\to {M}={L}\right)\right)$
34 13 33 sylbi ${⊢}\left|{A}\right|\in {ℕ}_{0}\to \left({M}\in \left(0\dots {L}+0\right)\to \left({L}\le {M}\to {M}={L}\right)\right)$
35 11 34 syl ${⊢}{A}\in \mathrm{Word}{V}\to \left({M}\in \left(0\dots {L}+0\right)\to \left({L}\le {M}\to {M}={L}\right)\right)$
36 35 imp ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {L}+0\right)\right)\to \left({L}\le {M}\to {M}={L}\right)$
37 elfznn0 ${⊢}{M}\in \left(0\dots {L}+0\right)\to {M}\in {ℕ}_{0}$
38 swrd00 ${⊢}\varnothing \mathrm{substr}⟨0,0⟩=\varnothing$
39 swrd00 ${⊢}{A}\mathrm{substr}⟨{L},{L}⟩=\varnothing$
40 38 39 eqtr4i ${⊢}\varnothing \mathrm{substr}⟨0,0⟩={A}\mathrm{substr}⟨{L},{L}⟩$
41 nn0cn ${⊢}{L}\in {ℕ}_{0}\to {L}\in ℂ$
42 41 subidd ${⊢}{L}\in {ℕ}_{0}\to {L}-{L}=0$
43 42 opeq1d ${⊢}{L}\in {ℕ}_{0}\to ⟨{L}-{L},0⟩=⟨0,0⟩$
44 43 oveq2d ${⊢}{L}\in {ℕ}_{0}\to \varnothing \mathrm{substr}⟨{L}-{L},0⟩=\varnothing \mathrm{substr}⟨0,0⟩$
45 41 addid1d ${⊢}{L}\in {ℕ}_{0}\to {L}+0={L}$
46 45 opeq2d ${⊢}{L}\in {ℕ}_{0}\to ⟨{L},{L}+0⟩=⟨{L},{L}⟩$
47 46 oveq2d ${⊢}{L}\in {ℕ}_{0}\to {A}\mathrm{substr}⟨{L},{L}+0⟩={A}\mathrm{substr}⟨{L},{L}⟩$
48 40 44 47 3eqtr4a ${⊢}{L}\in {ℕ}_{0}\to \varnothing \mathrm{substr}⟨{L}-{L},0⟩={A}\mathrm{substr}⟨{L},{L}+0⟩$
49 48 a1i ${⊢}{M}={L}\to \left({L}\in {ℕ}_{0}\to \varnothing \mathrm{substr}⟨{L}-{L},0⟩={A}\mathrm{substr}⟨{L},{L}+0⟩\right)$
50 eleq1 ${⊢}{M}={L}\to \left({M}\in {ℕ}_{0}↔{L}\in {ℕ}_{0}\right)$
51 oveq1 ${⊢}{M}={L}\to {M}-{L}={L}-{L}$
52 51 opeq1d ${⊢}{M}={L}\to ⟨{M}-{L},0⟩=⟨{L}-{L},0⟩$
53 52 oveq2d ${⊢}{M}={L}\to \varnothing \mathrm{substr}⟨{M}-{L},0⟩=\varnothing \mathrm{substr}⟨{L}-{L},0⟩$
54 opeq1 ${⊢}{M}={L}\to ⟨{M},{L}+0⟩=⟨{L},{L}+0⟩$
55 54 oveq2d ${⊢}{M}={L}\to {A}\mathrm{substr}⟨{M},{L}+0⟩={A}\mathrm{substr}⟨{L},{L}+0⟩$
56 53 55 eqeq12d ${⊢}{M}={L}\to \left(\varnothing \mathrm{substr}⟨{M}-{L},0⟩={A}\mathrm{substr}⟨{M},{L}+0⟩↔\varnothing \mathrm{substr}⟨{L}-{L},0⟩={A}\mathrm{substr}⟨{L},{L}+0⟩\right)$
57 49 50 56 3imtr4d ${⊢}{M}={L}\to \left({M}\in {ℕ}_{0}\to \varnothing \mathrm{substr}⟨{M}-{L},0⟩={A}\mathrm{substr}⟨{M},{L}+0⟩\right)$
58 57 com12 ${⊢}{M}\in {ℕ}_{0}\to \left({M}={L}\to \varnothing \mathrm{substr}⟨{M}-{L},0⟩={A}\mathrm{substr}⟨{M},{L}+0⟩\right)$
59 58 a1d ${⊢}{M}\in {ℕ}_{0}\to \left({A}\in \mathrm{Word}{V}\to \left({M}={L}\to \varnothing \mathrm{substr}⟨{M}-{L},0⟩={A}\mathrm{substr}⟨{M},{L}+0⟩\right)\right)$
60 37 59 syl ${⊢}{M}\in \left(0\dots {L}+0\right)\to \left({A}\in \mathrm{Word}{V}\to \left({M}={L}\to \varnothing \mathrm{substr}⟨{M}-{L},0⟩={A}\mathrm{substr}⟨{M},{L}+0⟩\right)\right)$
61 60 impcom ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {L}+0\right)\right)\to \left({M}={L}\to \varnothing \mathrm{substr}⟨{M}-{L},0⟩={A}\mathrm{substr}⟨{M},{L}+0⟩\right)$
62 36 61 syld ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {L}+0\right)\right)\to \left({L}\le {M}\to \varnothing \mathrm{substr}⟨{M}-{L},0⟩={A}\mathrm{substr}⟨{M},{L}+0⟩\right)$
63 62 imp ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {L}+0\right)\right)\wedge {L}\le {M}\right)\to \varnothing \mathrm{substr}⟨{M}-{L},0⟩={A}\mathrm{substr}⟨{M},{L}+0⟩$
64 swrdcl ${⊢}{A}\in \mathrm{Word}{V}\to {A}\mathrm{substr}⟨{M},{L}⟩\in \mathrm{Word}{V}$
65 ccatrid ${⊢}{A}\mathrm{substr}⟨{M},{L}⟩\in \mathrm{Word}{V}\to \left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing ={A}\mathrm{substr}⟨{M},{L}⟩$
66 64 65 syl ${⊢}{A}\in \mathrm{Word}{V}\to \left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing ={A}\mathrm{substr}⟨{M},{L}⟩$
67 13 41 sylbi ${⊢}\left|{A}\right|\in {ℕ}_{0}\to {L}\in ℂ$
68 11 67 syl ${⊢}{A}\in \mathrm{Word}{V}\to {L}\in ℂ$
69 addid1 ${⊢}{L}\in ℂ\to {L}+0={L}$
70 69 eqcomd ${⊢}{L}\in ℂ\to {L}={L}+0$
71 68 70 syl ${⊢}{A}\in \mathrm{Word}{V}\to {L}={L}+0$
72 71 opeq2d ${⊢}{A}\in \mathrm{Word}{V}\to ⟨{M},{L}⟩=⟨{M},{L}+0⟩$
73 72 oveq2d ${⊢}{A}\in \mathrm{Word}{V}\to {A}\mathrm{substr}⟨{M},{L}⟩={A}\mathrm{substr}⟨{M},{L}+0⟩$
74 66 73 eqtrd ${⊢}{A}\in \mathrm{Word}{V}\to \left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing ={A}\mathrm{substr}⟨{M},{L}+0⟩$
75 74 adantr ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {L}+0\right)\right)\to \left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing ={A}\mathrm{substr}⟨{M},{L}+0⟩$
76 75 adantr ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {L}+0\right)\right)\wedge ¬{L}\le {M}\right)\to \left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing ={A}\mathrm{substr}⟨{M},{L}+0⟩$
77 63 76 ifeqda ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {L}+0\right)\right)\to if\left({L}\le {M},\varnothing \mathrm{substr}⟨{M}-{L},0⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing \right)={A}\mathrm{substr}⟨{M},{L}+0⟩$
78 77 ex ${⊢}{A}\in \mathrm{Word}{V}\to \left({M}\in \left(0\dots {L}+0\right)\to if\left({L}\le {M},\varnothing \mathrm{substr}⟨{M}-{L},0⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing \right)={A}\mathrm{substr}⟨{M},{L}+0⟩\right)$
79 78 ad3antrrr ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{B}\right|=0\right)\wedge {B}=\varnothing \right)\to \left({M}\in \left(0\dots {L}+0\right)\to if\left({L}\le {M},\varnothing \mathrm{substr}⟨{M}-{L},0⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing \right)={A}\mathrm{substr}⟨{M},{L}+0⟩\right)$
80 oveq2 ${⊢}\left|{B}\right|=0\to {L}+\left|{B}\right|={L}+0$
81 80 oveq2d ${⊢}\left|{B}\right|=0\to \left(0\dots {L}+\left|{B}\right|\right)=\left(0\dots {L}+0\right)$
82 81 eleq2d ${⊢}\left|{B}\right|=0\to \left({M}\in \left(0\dots {L}+\left|{B}\right|\right)↔{M}\in \left(0\dots {L}+0\right)\right)$
83 82 adantr ${⊢}\left(\left|{B}\right|=0\wedge {B}=\varnothing \right)\to \left({M}\in \left(0\dots {L}+\left|{B}\right|\right)↔{M}\in \left(0\dots {L}+0\right)\right)$
84 simpr ${⊢}\left(\left|{B}\right|=0\wedge {B}=\varnothing \right)\to {B}=\varnothing$
85 opeq2 ${⊢}\left|{B}\right|=0\to ⟨{M}-{L},\left|{B}\right|⟩=⟨{M}-{L},0⟩$
86 85 adantr ${⊢}\left(\left|{B}\right|=0\wedge {B}=\varnothing \right)\to ⟨{M}-{L},\left|{B}\right|⟩=⟨{M}-{L},0⟩$
87 84 86 oveq12d ${⊢}\left(\left|{B}\right|=0\wedge {B}=\varnothing \right)\to {B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩=\varnothing \mathrm{substr}⟨{M}-{L},0⟩$
88 oveq2 ${⊢}{B}=\varnothing \to \left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}=\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing$
89 88 adantl ${⊢}\left(\left|{B}\right|=0\wedge {B}=\varnothing \right)\to \left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}=\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing$
90 87 89 ifeq12d ${⊢}\left(\left|{B}\right|=0\wedge {B}=\varnothing \right)\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)=if\left({L}\le {M},\varnothing \mathrm{substr}⟨{M}-{L},0⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing \right)$
91 80 opeq2d ${⊢}\left|{B}\right|=0\to ⟨{M},{L}+\left|{B}\right|⟩=⟨{M},{L}+0⟩$
92 91 oveq2d ${⊢}\left|{B}\right|=0\to {A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩={A}\mathrm{substr}⟨{M},{L}+0⟩$
93 92 adantr ${⊢}\left(\left|{B}\right|=0\wedge {B}=\varnothing \right)\to {A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩={A}\mathrm{substr}⟨{M},{L}+0⟩$
94 90 93 eqeq12d ${⊢}\left(\left|{B}\right|=0\wedge {B}=\varnothing \right)\to \left(if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩↔if\left({L}\le {M},\varnothing \mathrm{substr}⟨{M}-{L},0⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing \right)={A}\mathrm{substr}⟨{M},{L}+0⟩\right)$
95 83 94 imbi12d ${⊢}\left(\left|{B}\right|=0\wedge {B}=\varnothing \right)\to \left(\left({M}\in \left(0\dots {L}+\left|{B}\right|\right)\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)↔\left({M}\in \left(0\dots {L}+0\right)\to if\left({L}\le {M},\varnothing \mathrm{substr}⟨{M}-{L},0⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing \right)={A}\mathrm{substr}⟨{M},{L}+0⟩\right)\right)$
96 95 adantll ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{B}\right|=0\right)\wedge {B}=\varnothing \right)\to \left(\left({M}\in \left(0\dots {L}+\left|{B}\right|\right)\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)↔\left({M}\in \left(0\dots {L}+0\right)\to if\left({L}\le {M},\varnothing \mathrm{substr}⟨{M}-{L},0⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}\varnothing \right)={A}\mathrm{substr}⟨{M},{L}+0⟩\right)\right)$
97 79 96 mpbird ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{B}\right|=0\right)\wedge {B}=\varnothing \right)\to \left({M}\in \left(0\dots {L}+\left|{B}\right|\right)\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)$
98 10 97 mpdan ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left|{B}\right|=0\right)\to \left({M}\in \left(0\dots {L}+\left|{B}\right|\right)\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)$
99 98 ex ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to \left(\left|{B}\right|=0\to \left({M}\in \left(0\dots {L}+\left|{B}\right|\right)\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)\right)$
100 6 99 syld ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to \left(\left|{B}\right|\le 0\to \left({M}\in \left(0\dots {L}+\left|{B}\right|\right)\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)\right)$
101 100 com23 ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to \left({M}\in \left(0\dots {L}+\left|{B}\right|\right)\to \left(\left|{B}\right|\le 0\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)\right)$
102 101 imp ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge {M}\in \left(0\dots {L}+\left|{B}\right|\right)\right)\to \left(\left|{B}\right|\le 0\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)$
103 102 adantr ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge {M}\in \left(0\dots {L}+\left|{B}\right|\right)\right)\wedge {L}+\left|{B}\right|\le {L}\right)\to \left(\left|{B}\right|\le 0\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)$
104 1 eleq1i ${⊢}{L}\in {ℕ}_{0}↔\left|{A}\right|\in {ℕ}_{0}$
105 104 14 sylbir ${⊢}\left|{A}\right|\in {ℕ}_{0}\to {L}\in ℝ$
106 11 105 syl ${⊢}{A}\in \mathrm{Word}{V}\to {L}\in ℝ$
107 2 nn0red ${⊢}{B}\in \mathrm{Word}{V}\to \left|{B}\right|\in ℝ$
108 leaddle0 ${⊢}\left({L}\in ℝ\wedge \left|{B}\right|\in ℝ\right)\to \left({L}+\left|{B}\right|\le {L}↔\left|{B}\right|\le 0\right)$
109 106 107 108 syl2an ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to \left({L}+\left|{B}\right|\le {L}↔\left|{B}\right|\le 0\right)$
110 pm2.24 ${⊢}\left|{B}\right|\le 0\to \left(¬\left|{B}\right|\le 0\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)$
111 109 110 syl6bi ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to \left({L}+\left|{B}\right|\le {L}\to \left(¬\left|{B}\right|\le 0\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)\right)$
112 111 adantr ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge {M}\in \left(0\dots {L}+\left|{B}\right|\right)\right)\to \left({L}+\left|{B}\right|\le {L}\to \left(¬\left|{B}\right|\le 0\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)\right)$
113 112 imp ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge {M}\in \left(0\dots {L}+\left|{B}\right|\right)\right)\wedge {L}+\left|{B}\right|\le {L}\right)\to \left(¬\left|{B}\right|\le 0\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩\right)$
114 103 113 pm2.61d ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge {M}\in \left(0\dots {L}+\left|{B}\right|\right)\right)\wedge {L}+\left|{B}\right|\le {L}\right)\to if\left({L}\le {M},{B}\mathrm{substr}⟨{M}-{L},\left|{B}\right|⟩,\left({A}\mathrm{substr}⟨{M},{L}⟩\right)\mathrm{++}{B}\right)={A}\mathrm{substr}⟨{M},{L}+\left|{B}\right|⟩$