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 {\mathbb{N}}_0$$
3		nn0le0eq0	$$⊢\left|B\right|\in {\mathbb{N}}_0\to \left(\left|B\right|\le 0\leftrightarrow \left|B\right|=0\right)$$
4	3	biimpd	$$⊢\left|B\right|\in {\mathbb{N}}_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\leftrightarrow 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 {\mathbb{N}}_0$$
12	1	eqcomi	$$⊢\left|A\right|=L$$
13	12	eleq1i	$$⊢\left|A\right|\in {\mathbb{N}}_0\leftrightarrow L\in {\mathbb{N}}_0$$
14		nn0re	$$⊢L\in {\mathbb{N}}_0\to L\in ℝ$$
15		elfz2nn0	$$⊢M\in \left(0\dots L+0\right)\leftrightarrow \left(M\in {\mathbb{N}}_0\wedge L+0\in {\mathbb{N}}_0\wedge M\le L+0\right)$$
16		recn	$$⊢L\in ℝ\to L\in ℂ$$
17	16	addridd	$$⊢L\in ℝ\to L+0=L$$
18	17	breq2d	$$⊢L\in ℝ\to \left(M\le L+0\leftrightarrow M\le L\right)$$
19		nn0re	$$⊢M\in {\mathbb{N}}_0\to M\in ℝ$$
20	19	anim1i	$$⊢\left(M\in {\mathbb{N}}_0\wedge L\in ℝ\right)\to \left(M\in ℝ\wedge L\in ℝ\right)$$
21	20	ancoms	$$⊢\left(L\in ℝ\wedge M\in {\mathbb{N}}_0\right)\to \left(M\in ℝ\wedge L\in ℝ\right)$$
22		letri3	$$⊢\left(M\in ℝ\wedge L\in ℝ\right)\to \left(M=L\leftrightarrow \left(M\le L\wedge L\le M\right)\right)$$
23	21 22	syl	$$⊢\left(L\in ℝ\wedge M\in {\mathbb{N}}_0\right)\to \left(M=L\leftrightarrow \left(M\le L\wedge L\le M\right)\right)$$
24	23	biimprd	$$⊢\left(L\in ℝ\wedge M\in {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_0\to \left(L\le M\to M=L\right)\right)\right)$$
28	27	com3l	$$⊢M\le L+0\to \left(M\in {\mathbb{N}}_0\to \left(L\in ℝ\to \left(L\le M\to M=L\right)\right)\right)$$
29	28	impcom	$$⊢\left(M\in {\mathbb{N}}_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 {\mathbb{N}}_0\wedge L+0\in {\mathbb{N}}_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 {\mathbb{N}}_0\wedge L+0\in {\mathbb{N}}_0\wedge M\le L+0\right)\to \left(L\le M\to M=L\right)\right)$$
32	15 31	biimtrid	$$⊢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 {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_0\to L\in ℂ$$
42	41	subidd	$$⊢L\in {\mathbb{N}}_0\to L-L=0$$
43	42	opeq1d	$$⊢L\in {\mathbb{N}}_0\to ⟨L-L,0⟩=⟨0,0⟩$$
44	43	oveq2d	$$⊢L\in {\mathbb{N}}_0\to \varnothing \mathrm{substr}⟨L-L,0⟩=\varnothing \mathrm{substr}⟨0,0⟩$$
45	41	addridd	$$⊢L\in {\mathbb{N}}_0\to L+0=L$$
46	45	opeq2d	$$⊢L\in {\mathbb{N}}_0\to ⟨L,L+0⟩=⟨L,L⟩$$
47	46	oveq2d	$$⊢L\in {\mathbb{N}}_0\to A\mathrm{substr}⟨L,L+0⟩=A\mathrm{substr}⟨L,L⟩$$
48	40 44 47	3eqtr4a	$$⊢L\in {\mathbb{N}}_0\to \varnothing \mathrm{substr}⟨L-L,0⟩=A\mathrm{substr}⟨L,L+0⟩$$
49	48	a1i	$$⊢M=L\to \left(L\in {\mathbb{N}}_0\to \varnothing \mathrm{substr}⟨L-L,0⟩=A\mathrm{substr}⟨L,L+0⟩\right)$$
50		eleq1	$$⊢M=L\to \left(M\in {\mathbb{N}}_0\leftrightarrow L\in {\mathbb{N}}_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⟩\leftrightarrow \varnothing \mathrm{substr}⟨L-L,0⟩=A\mathrm{substr}⟨L,L+0⟩\right)$$
57	49 50 56	3imtr4d	$$⊢M=L\to \left(M\in {\mathbb{N}}_0\to \varnothing \mathrm{substr}⟨M-L,0⟩=A\mathrm{substr}⟨M,L+0⟩\right)$$
58	57	com12	$$⊢M\in {\mathbb{N}}_0\to \left(M=L\to \varnothing \mathrm{substr}⟨M-L,0⟩=A\mathrm{substr}⟨M,L+0⟩\right)$$
59	58	a1d	$$⊢M\in {\mathbb{N}}_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 {\mathbb{N}}_0\to L\in ℂ$$
68	11 67	syl	$$⊢A\in \mathrm{Word}V\to L\in ℂ$$
69		addrid	$$⊢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 \neg 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)\leftrightarrow 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)\leftrightarrow 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|⟩\leftrightarrow 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)\leftrightarrow \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)\leftrightarrow \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 {\mathbb{N}}_0\leftrightarrow \left|A\right|\in {\mathbb{N}}_0$$
105	104 14	sylbir	$$⊢\left|A\right|\in {\mathbb{N}}_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\leftrightarrow \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\leftrightarrow \left|B\right|\le 0\right)$$
110		pm2.24	$$⊢\left|B\right|\le 0\to \left(\neg \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	biimtrdi	$$⊢\left(A\in \mathrm{Word}V\wedge B\in \mathrm{Word}V\right)\to \left(L+\left|B\right|\le L\to \left(\neg \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(\neg \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(\neg \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|⟩$$