swrdccatin2

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

		Ref	Expression
	Hypothesis	swrdccatin2.l	$⊢ L = \|A\|$
	Assertion	swrdccatin2	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (L \dots N) \land N \in (L \dots L + \|B\|)) \to (A ++ B) substr ⟨M, N⟩ = B substr ⟨M - L, N - L⟩)$

Proof

Step	Hyp	Ref	Expression
1		swrdccatin2.l	$⊢ L = \|A\|$
2		oveq1	$⊢ L = \|A\| \to (L \dots N) = (\|A\| \dots N)$
3	2	eleq2d	$⊢ L = \|A\| \to (M \in (L \dots N) \leftrightarrow M \in (\|A\| \dots N))$
4		id	$⊢ L = \|A\| \to L = \|A\|$
5		oveq1	$⊢ L = \|A\| \to L + \|B\| = \|A\| + \|B\|$
6	4 5	oveq12d	$⊢ L = \|A\| \to (L \dots L + \|B\|) = (\|A\| \dots \|A\| + \|B\|)$
7	6	eleq2d	$⊢ L = \|A\| \to (N \in (L \dots L + \|B\|) \leftrightarrow N \in (\|A\| \dots \|A\| + \|B\|))$
8	3 7	anbi12d	$⊢ L = \|A\| \to ((M \in (L \dots N) \land N \in (L \dots L + \|B\|)) \leftrightarrow (M \in (\|A\| \dots N) \land N \in (\|A\| \dots \|A\| + \|B\|)))$
9	1 8	ax-mp	$⊢ (M \in (L \dots N) \land N \in (L \dots L + \|B\|)) \leftrightarrow (M \in (\|A\| \dots N) \land N \in (\|A\| \dots \|A\| + \|B\|))$
10		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
11		elnn0uz	$⊢ \|A\| \in ℕ_{0} \leftrightarrow \|A\| \in ℤ_{\geq 0}$
12		fzss1	$⊢ \|A\| \in ℤ_{\geq 0} \to (\|A\| \dots N) \subseteq (0 \dots N)$
13	11 12	sylbi	$⊢ \|A\| \in ℕ_{0} \to (\|A\| \dots N) \subseteq (0 \dots N)$
14	13	sseld	$⊢ \|A\| \in ℕ_{0} \to (M \in (\|A\| \dots N) \to M \in (0 \dots N))$
15		fzss1	$⊢ \|A\| \in ℤ_{\geq 0} \to (\|A\| \dots \|A\| + \|B\|) \subseteq (0 \dots \|A\| + \|B\|)$
16	11 15	sylbi	$⊢ \|A\| \in ℕ_{0} \to (\|A\| \dots \|A\| + \|B\|) \subseteq (0 \dots \|A\| + \|B\|)$
17	16	sseld	$⊢ \|A\| \in ℕ_{0} \to (N \in (\|A\| \dots \|A\| + \|B\|) \to N \in (0 \dots \|A\| + \|B\|))$
18	14 17	anim12d	$⊢ \|A\| \in ℕ_{0} \to ((M \in (\|A\| \dots N) \land N \in (\|A\| \dots \|A\| + \|B\|)) \to (M \in (0 \dots N) \land N \in (0 \dots \|A\| + \|B\|)))$
19	10 18	syl	$⊢ A \in Word V \to ((M \in (\|A\| \dots N) \land N \in (\|A\| \dots \|A\| + \|B\|)) \to (M \in (0 \dots N) \land N \in (0 \dots \|A\| + \|B\|)))$
20	19	adantr	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (\|A\| \dots N) \land N \in (\|A\| \dots \|A\| + \|B\|)) \to (M \in (0 \dots N) \land N \in (0 \dots \|A\| + \|B\|)))$
21	9 20	biimtrid	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (L \dots N) \land N \in (L \dots L + \|B\|)) \to (M \in (0 \dots N) \land N \in (0 \dots \|A\| + \|B\|)))$
22	21	imp	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to (M \in (0 \dots N) \land N \in (0 \dots \|A\| + \|B\|))$
23		swrdccatfn	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots \|A\| + \|B\|))) \to ((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - M)$
24	22 23	syldan	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to ((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - M)$
25		fzmmmeqm	$⊢ M \in (L \dots N) \to N - L - (M - L) = N - M$
26	25	oveq2d	$⊢ M \in (L \dots N) \to (0 ..^N - L - (M - L)) = (0 ..^N - M)$
27	26	fneq2d	$⊢ M \in (L \dots N) \to (((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - L - (M - L)) \leftrightarrow ((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - M))$
28	27	ad2antrl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to (((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - L - (M - L)) \leftrightarrow ((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - M))$
29	24 28	mpbird	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to ((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - L - (M - L))$
30		simplr	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to B \in Word V$
31		elfzmlbm	$⊢ M \in (L \dots N) \to M - L \in (0 \dots N - L)$
32	31	ad2antrl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to M - L \in (0 \dots N - L)$
33		lencl	$⊢ B \in Word V \to \|B\| \in ℕ_{0}$
34	33	nn0zd	$⊢ B \in Word V \to \|B\| \in ℤ$
35	34	adantl	$⊢ (A \in Word V \land B \in Word V) \to \|B\| \in ℤ$
36		elfzmlbp	$⊢ (\|B\| \in ℤ \land N \in (L \dots L + \|B\|)) \to N - L \in (0 \dots \|B\|)$
37	35 36	sylan	$⊢ ((A \in Word V \land B \in Word V) \land N \in (L \dots L + \|B\|)) \to N - L \in (0 \dots \|B\|)$
38	37	adantrl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to N - L \in (0 \dots \|B\|)$
39		swrdvalfn	$⊢ (B \in Word V \land M - L \in (0 \dots N - L) \land N - L \in (0 \dots \|B\|)) \to (B substr ⟨M - L, N - L⟩) Fn (0 ..^N - L - (M - L))$
40	30 32 38 39	syl3anc	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to (B substr ⟨M - L, N - L⟩) Fn (0 ..^N - L - (M - L))$
41		simpll	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to (A \in Word V \land B \in Word V)$
42		elfzelz	$⊢ M \in (L \dots N) \to M \in ℤ$
43		zaddcl	$⊢ (k \in ℤ \land M \in ℤ) \to k + M \in ℤ$
44	43	expcom	$⊢ M \in ℤ \to (k \in ℤ \to k + M \in ℤ)$
45	42 44	syl	$⊢ M \in (L \dots N) \to (k \in ℤ \to k + M \in ℤ)$
46	45	ad2antrl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to (k \in ℤ \to k + M \in ℤ)$
47		elfzoelz	$⊢ k \in (0 ..^N - L - (M - L)) \to k \in ℤ$
48	46 47	impel	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to k + M \in ℤ$
49		df-3an	$⊢ (A \in Word V \land B \in Word V \land k + M \in ℤ) \leftrightarrow ((A \in Word V \land B \in Word V) \land k + M \in ℤ)$
50	41 48 49	sylanbrc	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to (A \in Word V \land B \in Word V \land k + M \in ℤ)$
51		ccatsymb	$⊢ (A \in Word V \land B \in Word V \land k + M \in ℤ) \to (A ++ B) (k + M) = if (k + M < \|A\|, A (k + M), B (k + M - \|A\|))$
52	50 51	syl	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to (A ++ B) (k + M) = if (k + M < \|A\|, A (k + M), B (k + M - \|A\|))$
53		elfz2	$⊢ M \in (L \dots N) \leftrightarrow ((L \in ℤ \land N \in ℤ \land M \in ℤ) \land (L \leq M \land M \leq N))$
54		zre	$⊢ L \in ℤ \to L \in ℝ$
55		zre	$⊢ M \in ℤ \to M \in ℝ$
56	54 55	anim12i	$⊢ (L \in ℤ \land M \in ℤ) \to (L \in ℝ \land M \in ℝ)$
57		elnn0z	$⊢ k \in ℕ_{0} \leftrightarrow (k \in ℤ \land 0 \leq k)$
58		zre	$⊢ k \in ℤ \to k \in ℝ$
59		0re	$⊢ 0 \in ℝ$
60	59	jctl	$⊢ L \in ℝ \to (0 \in ℝ \land L \in ℝ)$
61	60	ad2antrl	$⊢ (k \in ℝ \land (L \in ℝ \land M \in ℝ)) \to (0 \in ℝ \land L \in ℝ)$
62		id	$⊢ (k \in ℝ \land M \in ℝ) \to (k \in ℝ \land M \in ℝ)$
63	62	adantrl	$⊢ (k \in ℝ \land (L \in ℝ \land M \in ℝ)) \to (k \in ℝ \land M \in ℝ)$
64		le2add	$⊢ ((0 \in ℝ \land L \in ℝ) \land (k \in ℝ \land M \in ℝ)) \to ((0 \leq k \land L \leq M) \to 0 + L \leq k + M)$
65	61 63 64	syl2anc	$⊢ (k \in ℝ \land (L \in ℝ \land M \in ℝ)) \to ((0 \leq k \land L \leq M) \to 0 + L \leq k + M)$
66		recn	$⊢ L \in ℝ \to L \in ℂ$
67	66	addlidd	$⊢ L \in ℝ \to 0 + L = L$
68	67	ad2antrl	$⊢ (k \in ℝ \land (L \in ℝ \land M \in ℝ)) \to 0 + L = L$
69	68	breq1d	$⊢ (k \in ℝ \land (L \in ℝ \land M \in ℝ)) \to (0 + L \leq k + M \leftrightarrow L \leq k + M)$
70	65 69	sylibd	$⊢ (k \in ℝ \land (L \in ℝ \land M \in ℝ)) \to ((0 \leq k \land L \leq M) \to L \leq k + M)$
71		simprl	$⊢ (k \in ℝ \land (L \in ℝ \land M \in ℝ)) \to L \in ℝ$
72		readdcl	$⊢ (k \in ℝ \land M \in ℝ) \to k + M \in ℝ$
73	72	adantrl	$⊢ (k \in ℝ \land (L \in ℝ \land M \in ℝ)) \to k + M \in ℝ$
74	71 73	lenltd	$⊢ (k \in ℝ \land (L \in ℝ \land M \in ℝ)) \to (L \leq k + M \leftrightarrow \neg k + M < L)$
75	70 74	sylibd	$⊢ (k \in ℝ \land (L \in ℝ \land M \in ℝ)) \to ((0 \leq k \land L \leq M) \to \neg k + M < L)$
76	75	expd	$⊢ (k \in ℝ \land (L \in ℝ \land M \in ℝ)) \to (0 \leq k \to (L \leq M \to \neg k + M < L))$
77	76	com12	$⊢ 0 \leq k \to ((k \in ℝ \land (L \in ℝ \land M \in ℝ)) \to (L \leq M \to \neg k + M < L))$
78	77	expd	$⊢ 0 \leq k \to (k \in ℝ \to ((L \in ℝ \land M \in ℝ) \to (L \leq M \to \neg k + M < L)))$
79	58 78	mpan9	$⊢ (k \in ℤ \land 0 \leq k) \to ((L \in ℝ \land M \in ℝ) \to (L \leq M \to \neg k + M < L))$
80	57 79	sylbi	$⊢ k \in ℕ_{0} \to ((L \in ℝ \land M \in ℝ) \to (L \leq M \to \neg k + M < L))$
81	56 80	mpan9	$⊢ ((L \in ℤ \land M \in ℤ) \land k \in ℕ_{0}) \to (L \leq M \to \neg k + M < L)$
82	1	breq2i	$⊢ k + M < L \leftrightarrow k + M < \|A\|$
83	82	notbii	$⊢ \neg k + M < L \leftrightarrow \neg k + M < \|A\|$
84	81 83	imbitrdi	$⊢ ((L \in ℤ \land M \in ℤ) \land k \in ℕ_{0}) \to (L \leq M \to \neg k + M < \|A\|)$
85	84	ex	$⊢ (L \in ℤ \land M \in ℤ) \to (k \in ℕ_{0} \to (L \leq M \to \neg k + M < \|A\|))$
86	85	com23	$⊢ (L \in ℤ \land M \in ℤ) \to (L \leq M \to (k \in ℕ_{0} \to \neg k + M < \|A\|))$
87	86	3adant2	$⊢ (L \in ℤ \land N \in ℤ \land M \in ℤ) \to (L \leq M \to (k \in ℕ_{0} \to \neg k + M < \|A\|))$
88	87	imp	$⊢ ((L \in ℤ \land N \in ℤ \land M \in ℤ) \land L \leq M) \to (k \in ℕ_{0} \to \neg k + M < \|A\|)$
89	88	adantrr	$⊢ ((L \in ℤ \land N \in ℤ \land M \in ℤ) \land (L \leq M \land M \leq N)) \to (k \in ℕ_{0} \to \neg k + M < \|A\|)$
90	53 89	sylbi	$⊢ M \in (L \dots N) \to (k \in ℕ_{0} \to \neg k + M < \|A\|)$
91	90	ad2antrl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to (k \in ℕ_{0} \to \neg k + M < \|A\|)$
92		elfzonn0	$⊢ k \in (0 ..^N - L - (M - L)) \to k \in ℕ_{0}$
93	91 92	impel	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to \neg k + M < \|A\|$
94	93	iffalsed	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to if (k + M < \|A\|, A (k + M), B (k + M - \|A\|)) = B (k + M - \|A\|)$
95		zcn	$⊢ k \in ℤ \to k \in ℂ$
96	95	adantl	$⊢ ((L \in ℤ \land M \in ℤ) \land k \in ℤ) \to k \in ℂ$
97		zcn	$⊢ M \in ℤ \to M \in ℂ$
98	97	ad2antlr	$⊢ ((L \in ℤ \land M \in ℤ) \land k \in ℤ) \to M \in ℂ$
99		zcn	$⊢ L \in ℤ \to L \in ℂ$
100	99	ad2antrr	$⊢ ((L \in ℤ \land M \in ℤ) \land k \in ℤ) \to L \in ℂ$
101	96 98 100	addsubassd	$⊢ ((L \in ℤ \land M \in ℤ) \land k \in ℤ) \to k + M - L = k + M - L$
102		oveq2	$⊢ L = \|A\| \to k + M - L = k + M - \|A\|$
103	102	eqeq1d	$⊢ L = \|A\| \to (k + M - L = k + M - L \leftrightarrow k + M - \|A\| = k + M - L)$
104	101 103	imbitrid	$⊢ L = \|A\| \to (((L \in ℤ \land M \in ℤ) \land k \in ℤ) \to k + M - \|A\| = k + M - L)$
105	1 104	ax-mp	$⊢ ((L \in ℤ \land M \in ℤ) \land k \in ℤ) \to k + M - \|A\| = k + M - L$
106	105	ex	$⊢ (L \in ℤ \land M \in ℤ) \to (k \in ℤ \to k + M - \|A\| = k + M - L)$
107	106	3adant2	$⊢ (L \in ℤ \land N \in ℤ \land M \in ℤ) \to (k \in ℤ \to k + M - \|A\| = k + M - L)$
108	107	adantr	$⊢ ((L \in ℤ \land N \in ℤ \land M \in ℤ) \land (L \leq M \land M \leq N)) \to (k \in ℤ \to k + M - \|A\| = k + M - L)$
109	53 108	sylbi	$⊢ M \in (L \dots N) \to (k \in ℤ \to k + M - \|A\| = k + M - L)$
110	109	ad2antrl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to (k \in ℤ \to k + M - \|A\| = k + M - L)$
111	110 47	impel	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to k + M - \|A\| = k + M - L$
112	111	fveq2d	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to B (k + M - \|A\|) = B (k + M - L)$
113	52 94 112	3eqtrd	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to (A ++ B) (k + M) = B (k + M - L)$
114		ccatcl	$⊢ (A \in Word V \land B \in Word V) \to A ++ B \in Word V$
115	114	adantr	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to A ++ B \in Word V$
116	11	biimpi	$⊢ \|A\| \in ℕ_{0} \to \|A\| \in ℤ_{\geq 0}$
117	1 116	eqeltrid	$⊢ \|A\| \in ℕ_{0} \to L \in ℤ_{\geq 0}$
118		fzss1	$⊢ L \in ℤ_{\geq 0} \to (L \dots N) \subseteq (0 \dots N)$
119	10 117 118	3syl	$⊢ A \in Word V \to (L \dots N) \subseteq (0 \dots N)$
120	119	sselda	$⊢ (A \in Word V \land M \in (L \dots N)) \to M \in (0 \dots N)$
121	120	ad2ant2r	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to M \in (0 \dots N)$
122	1 7	ax-mp	$⊢ N \in (L \dots L + \|B\|) \leftrightarrow N \in (\|A\| \dots \|A\| + \|B\|)$
123	10 116 15	3syl	$⊢ A \in Word V \to (\|A\| \dots \|A\| + \|B\|) \subseteq (0 \dots \|A\| + \|B\|)$
124	123	adantr	$⊢ (A \in Word V \land B \in Word V) \to (\|A\| \dots \|A\| + \|B\|) \subseteq (0 \dots \|A\| + \|B\|)$
125	124	sseld	$⊢ (A \in Word V \land B \in Word V) \to (N \in (\|A\| \dots \|A\| + \|B\|) \to N \in (0 \dots \|A\| + \|B\|))$
126	125	impcom	$⊢ (N \in (\|A\| \dots \|A\| + \|B\|) \land (A \in Word V \land B \in Word V)) \to N \in (0 \dots \|A\| + \|B\|)$
127		ccatlen	$⊢ (A \in Word V \land B \in Word V) \to \|A ++ B\| = \|A\| + \|B\|$
128	127	oveq2d	$⊢ (A \in Word V \land B \in Word V) \to (0 \dots \|A ++ B\|) = (0 \dots \|A\| + \|B\|)$
129	128	eleq2d	$⊢ (A \in Word V \land B \in Word V) \to (N \in (0 \dots \|A ++ B\|) \leftrightarrow N \in (0 \dots \|A\| + \|B\|))$
130	129	adantl	$⊢ (N \in (\|A\| \dots \|A\| + \|B\|) \land (A \in Word V \land B \in Word V)) \to (N \in (0 \dots \|A ++ B\|) \leftrightarrow N \in (0 \dots \|A\| + \|B\|))$
131	126 130	mpbird	$⊢ (N \in (\|A\| \dots \|A\| + \|B\|) \land (A \in Word V \land B \in Word V)) \to N \in (0 \dots \|A ++ B\|)$
132	131	ex	$⊢ N \in (\|A\| \dots \|A\| + \|B\|) \to ((A \in Word V \land B \in Word V) \to N \in (0 \dots \|A ++ B\|))$
133	122 132	sylbi	$⊢ N \in (L \dots L + \|B\|) \to ((A \in Word V \land B \in Word V) \to N \in (0 \dots \|A ++ B\|))$
134	133	impcom	$⊢ ((A \in Word V \land B \in Word V) \land N \in (L \dots L + \|B\|)) \to N \in (0 \dots \|A ++ B\|)$
135	134	adantrl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to N \in (0 \dots \|A ++ B\|)$
136	115 121 135	3jca	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to (A ++ B \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A ++ B\|))$
137	26	eleq2d	$⊢ M \in (L \dots N) \to (k \in (0 ..^N - L - (M - L)) \leftrightarrow k \in (0 ..^N - M))$
138	137	ad2antrl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to (k \in (0 ..^N - L - (M - L)) \leftrightarrow k \in (0 ..^N - M))$
139	138	biimpa	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to k \in (0 ..^N - M)$
140		swrdfv	$⊢ ((A ++ B \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A ++ B\|)) \land k \in (0 ..^N - M)) \to ((A ++ B) substr ⟨M, N⟩) (k) = (A ++ B) (k + M)$
141	136 139 140	syl2an2r	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to ((A ++ B) substr ⟨M, N⟩) (k) = (A ++ B) (k + M)$
142	34 36	sylan	$⊢ (B \in Word V \land N \in (L \dots L + \|B\|)) \to N - L \in (0 \dots \|B\|)$
143	142	ad2ant2l	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to N - L \in (0 \dots \|B\|)$
144	30 32 143	3jca	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to (B \in Word V \land M - L \in (0 \dots N - L) \land N - L \in (0 \dots \|B\|))$
145		swrdfv	$⊢ ((B \in Word V \land M - L \in (0 \dots N - L) \land N - L \in (0 \dots \|B\|)) \land k \in (0 ..^N - L - (M - L))) \to (B substr ⟨M - L, N - L⟩) (k) = B (k + M - L)$
146	144 145	sylan	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to (B substr ⟨M - L, N - L⟩) (k) = B (k + M - L)$
147	113 141 146	3eqtr4d	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - L - (M - L))) \to ((A ++ B) substr ⟨M, N⟩) (k) = (B substr ⟨M - L, N - L⟩) (k)$
148	29 40 147	eqfnfvd	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (L \dots N) \land N \in (L \dots L + \|B\|))) \to (A ++ B) substr ⟨M, N⟩ = B substr ⟨M - L, N - L⟩$
149	148	ex	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (L \dots N) \land N \in (L \dots L + \|B\|)) \to (A ++ B) substr ⟨M, N⟩ = B substr ⟨M - L, N - L⟩)$

Metamath Proof Explorer

Theorem swrdccatin2

Proof