swrdswrd

Description: A subword of a subword is a subword. (Contributed by Alexander van der Vekens, 4-Apr-2018)

		Ref	Expression
	Assertion	swrdswrd	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to ((K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to (W substr ⟨M, N⟩) substr ⟨K, L⟩ = W substr ⟨M + K, M + L⟩)$

Proof

Step	Hyp	Ref	Expression
1		swrdcl	$⊢ W \in Word V \to W substr ⟨M, N⟩ \in Word V$
2	1	3ad2ant1	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to W substr ⟨M, N⟩ \in Word V$
3	2	adantr	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to W substr ⟨M, N⟩ \in Word V$
4		elfz0ubfz0	$⊢ (K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to K \in (0 \dots L)$
5	4	adantl	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to K \in (0 \dots L)$
6		elfzuz	$⊢ K \in (0 \dots N - M) \to K \in ℤ_{\geq 0}$
7	6	adantl	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land K \in (0 \dots N - M)) \to K \in ℤ_{\geq 0}$
8		fzss1	$⊢ K \in ℤ_{\geq 0} \to (K \dots N - M) \subseteq (0 \dots N - M)$
9	7 8	syl	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land K \in (0 \dots N - M)) \to (K \dots N - M) \subseteq (0 \dots N - M)$
10	9	sseld	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land K \in (0 \dots N - M)) \to (L \in (K \dots N - M) \to L \in (0 \dots N - M))$
11	10	impr	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to L \in (0 \dots N - M)$
12		3ancomb	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \leftrightarrow (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|))$
13	12	biimpi	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|))$
14	13	adantr	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|))$
15		swrdlen	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to \|W substr ⟨M, N⟩\| = N - M$
16	14 15	syl	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to \|W substr ⟨M, N⟩\| = N - M$
17	16	oveq2d	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (0 \dots \|W substr ⟨M, N⟩\|) = (0 \dots N - M)$
18	11 17	eleqtrrd	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to L \in (0 \dots \|W substr ⟨M, N⟩\|)$
19		swrdval2	$⊢ (W substr ⟨M, N⟩ \in Word V \land K \in (0 \dots L) \land L \in (0 \dots \|W substr ⟨M, N⟩\|)) \to (W substr ⟨M, N⟩) substr ⟨K, L⟩ = (x \in (0 ..^L - K) ⟼ (W substr ⟨M, N⟩) (x + K))$
20	3 5 18 19	syl3anc	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (W substr ⟨M, N⟩) substr ⟨K, L⟩ = (x \in (0 ..^L - K) ⟼ (W substr ⟨M, N⟩) (x + K))$
21		fvex	$⊢ (W substr ⟨M, N⟩) (x + K) \in V$
22		eqid	$⊢ (x \in (0 ..^L - K) ⟼ (W substr ⟨M, N⟩) (x + K)) = (x \in (0 ..^L - K) ⟼ (W substr ⟨M, N⟩) (x + K))$
23	21 22	fnmpti	$⊢ (x \in (0 ..^L - K) ⟼ (W substr ⟨M, N⟩) (x + K)) Fn (0 ..^L - K)$
24	23	a1i	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (x \in (0 ..^L - K) ⟼ (W substr ⟨M, N⟩) (x + K)) Fn (0 ..^L - K)$
25		swrdswrdlem	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (W \in Word V \land M + K \in (0 \dots M + L) \land M + L \in (0 \dots \|W\|))$
26		swrdvalfn	$⊢ (W \in Word V \land M + K \in (0 \dots M + L) \land M + L \in (0 \dots \|W\|)) \to (W substr ⟨M + K, M + L⟩) Fn (0 ..^M + L - (M + K))$
27	25 26	syl	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (W substr ⟨M + K, M + L⟩) Fn (0 ..^M + L - (M + K))$
28		elfzelz	$⊢ M \in (0 \dots N) \to M \in ℤ$
29		elfzelz	$⊢ L \in (K \dots N - M) \to L \in ℤ$
30		elfzelz	$⊢ K \in (0 \dots N - M) \to K \in ℤ$
31		zcn	$⊢ M \in ℤ \to M \in ℂ$
32	31	adantr	$⊢ (M \in ℤ \land (L \in ℤ \land K \in ℤ)) \to M \in ℂ$
33		zcn	$⊢ L \in ℤ \to L \in ℂ$
34	33	ad2antrl	$⊢ (M \in ℤ \land (L \in ℤ \land K \in ℤ)) \to L \in ℂ$
35		zcn	$⊢ K \in ℤ \to K \in ℂ$
36	35	ad2antll	$⊢ (M \in ℤ \land (L \in ℤ \land K \in ℤ)) \to K \in ℂ$
37		pnpcan	$⊢ (M \in ℂ \land L \in ℂ \land K \in ℂ) \to M + L - (M + K) = L - K$
38	37	eqcomd	$⊢ (M \in ℂ \land L \in ℂ \land K \in ℂ) \to L - K = M + L - (M + K)$
39	32 34 36 38	syl3anc	$⊢ (M \in ℤ \land (L \in ℤ \land K \in ℤ)) \to L - K = M + L - (M + K)$
40	39	expcom	$⊢ (L \in ℤ \land K \in ℤ) \to (M \in ℤ \to L - K = M + L - (M + K))$
41	29 30 40	syl2anr	$⊢ (K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to (M \in ℤ \to L - K = M + L - (M + K))$
42	28 41	syl5com	$⊢ M \in (0 \dots N) \to ((K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to L - K = M + L - (M + K))$
43	42	3ad2ant3	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to ((K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to L - K = M + L - (M + K))$
44	43	imp	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to L - K = M + L - (M + K)$
45	44	oveq2d	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (0 ..^L - K) = (0 ..^M + L - (M + K))$
46	45	fneq2d	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to ((W substr ⟨M + K, M + L⟩) Fn (0 ..^L - K) \leftrightarrow (W substr ⟨M + K, M + L⟩) Fn (0 ..^M + L - (M + K)))$
47	27 46	mpbird	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (W substr ⟨M + K, M + L⟩) Fn (0 ..^L - K)$
48		simpr	$⊢ (((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \to y \in (0 ..^L - K)$
49		fvex	$⊢ W (y + K + M) \in V$
50		oveq1	$⊢ x = y \to x + K = y + K$
51	50	fvoveq1d	$⊢ x = y \to W (x + K + M) = W (y + K + M)$
52		eqid	$⊢ (x \in (0 ..^L - K) ⟼ W (x + K + M)) = (x \in (0 ..^L - K) ⟼ W (x + K + M))$
53	51 52	fvmptg	$⊢ (y \in (0 ..^L - K) \land W (y + K + M) \in V) \to (x \in (0 ..^L - K) ⟼ W (x + K + M)) (y) = W (y + K + M)$
54	48 49 53	sylancl	$⊢ (((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \to (x \in (0 ..^L - K) ⟼ W (x + K + M)) (y) = W (y + K + M)$
55		zcn	$⊢ y \in ℤ \to y \in ℂ$
56	55 31 35	3anim123i	$⊢ (y \in ℤ \land M \in ℤ \land K \in ℤ) \to (y \in ℂ \land M \in ℂ \land K \in ℂ)$
57	56	3expa	$⊢ ((y \in ℤ \land M \in ℤ) \land K \in ℤ) \to (y \in ℂ \land M \in ℂ \land K \in ℂ)$
58		add32r	$⊢ (y \in ℂ \land M \in ℂ \land K \in ℂ) \to y + M + K = y + K + M$
59	58	eqcomd	$⊢ (y \in ℂ \land M \in ℂ \land K \in ℂ) \to y + K + M = y + M + K$
60	57 59	syl	$⊢ ((y \in ℤ \land M \in ℤ) \land K \in ℤ) \to y + K + M = y + M + K$
61	60	exp31	$⊢ y \in ℤ \to (M \in ℤ \to (K \in ℤ \to y + K + M = y + M + K))$
62	61	com13	$⊢ K \in ℤ \to (M \in ℤ \to (y \in ℤ \to y + K + M = y + M + K))$
63	30 62	syl	$⊢ K \in (0 \dots N - M) \to (M \in ℤ \to (y \in ℤ \to y + K + M = y + M + K))$
64	63	adantr	$⊢ (K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to (M \in ℤ \to (y \in ℤ \to y + K + M = y + M + K))$
65	28 64	syl5com	$⊢ M \in (0 \dots N) \to ((K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to (y \in ℤ \to y + K + M = y + M + K))$
66	65	3ad2ant3	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to ((K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to (y \in ℤ \to y + K + M = y + M + K))$
67	66	imp	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (y \in ℤ \to y + K + M = y + M + K)$
68		elfzoelz	$⊢ y \in (0 ..^L - K) \to y \in ℤ$
69	67 68	impel	$⊢ (((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \to y + K + M = y + M + K$
70	69	fveq2d	$⊢ (((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \to W (y + K + M) = W (y + M + K)$
71	54 70	eqtrd	$⊢ (((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \to (x \in (0 ..^L - K) ⟼ W (x + K + M)) (y) = W (y + M + K)$
72	13	ad3antrrr	$⊢ ((((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \land x \in (0 ..^L - K)) \to (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|))$
73		elfz2nn0	$⊢ K \in (0 \dots N - M) \leftrightarrow (K \in ℕ_{0} \land N - M \in ℕ_{0} \land K \leq N - M)$
74		elfz2	$⊢ L \in (K \dots N - M) \leftrightarrow ((K \in ℤ \land N - M \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N - M))$
75		elfzo0	$⊢ x \in (0 ..^L - K) \leftrightarrow (x \in ℕ_{0} \land L - K \in ℕ \land x < L - K)$
76		nn0re	$⊢ x \in ℕ_{0} \to x \in ℝ$
77	76	ad2antrl	$⊢ (K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \to x \in ℝ$
78		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
79	78	adantr	$⊢ (K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \to K \in ℝ$
80		zre	$⊢ L \in ℤ \to L \in ℝ$
81	80	ad2antll	$⊢ (K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \to L \in ℝ$
82		ltaddsub	$⊢ (x \in ℝ \land K \in ℝ \land L \in ℝ) \to (x + K < L \leftrightarrow x < L - K)$
83	82	bicomd	$⊢ (x \in ℝ \land K \in ℝ \land L \in ℝ) \to (x < L - K \leftrightarrow x + K < L)$
84	77 79 81 83	syl3anc	$⊢ (K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \to (x < L - K \leftrightarrow x + K < L)$
85		nn0addcl	$⊢ (x \in ℕ_{0} \land K \in ℕ_{0}) \to x + K \in ℕ_{0}$
86	85	ex	$⊢ x \in ℕ_{0} \to (K \in ℕ_{0} \to x + K \in ℕ_{0})$
87	86	adantr	$⊢ (x \in ℕ_{0} \land L \in ℤ) \to (K \in ℕ_{0} \to x + K \in ℕ_{0})$
88	87	impcom	$⊢ (K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \to x + K \in ℕ_{0}$
89	88	ad3antrrr	$⊢ ((((K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \land x + K < L) \land N - M \in ℕ_{0}) \land L \leq N - M) \to x + K \in ℕ_{0}$
90		elnn0z	$⊢ x + K \in ℕ_{0} \leftrightarrow (x + K \in ℤ \land 0 \leq x + K)$
91		0red	$⊢ (x + K \in ℤ \land L \in ℤ) \to 0 \in ℝ$
92		zre	$⊢ x + K \in ℤ \to x + K \in ℝ$
93	92	adantr	$⊢ (x + K \in ℤ \land L \in ℤ) \to x + K \in ℝ$
94	80	adantl	$⊢ (x + K \in ℤ \land L \in ℤ) \to L \in ℝ$
95		lelttr	$⊢ (0 \in ℝ \land x + K \in ℝ \land L \in ℝ) \to ((0 \leq x + K \land x + K < L) \to 0 < L)$
96	91 93 94 95	syl3anc	$⊢ (x + K \in ℤ \land L \in ℤ) \to ((0 \leq x + K \land x + K < L) \to 0 < L)$
97		0red	$⊢ (L \in ℤ \land N - M \in ℕ_{0}) \to 0 \in ℝ$
98	80	adantr	$⊢ (L \in ℤ \land N - M \in ℕ_{0}) \to L \in ℝ$
99		nn0re	$⊢ N - M \in ℕ_{0} \to N - M \in ℝ$
100	99	adantl	$⊢ (L \in ℤ \land N - M \in ℕ_{0}) \to N - M \in ℝ$
101		ltletr	$⊢ (0 \in ℝ \land L \in ℝ \land N - M \in ℝ) \to ((0 < L \land L \leq N - M) \to 0 < N - M)$
102	97 98 100 101	syl3anc	$⊢ (L \in ℤ \land N - M \in ℕ_{0}) \to ((0 < L \land L \leq N - M) \to 0 < N - M)$
103		elnnnn0b	$⊢ N - M \in ℕ \leftrightarrow (N - M \in ℕ_{0} \land 0 < N - M)$
104	103	simplbi2	$⊢ N - M \in ℕ_{0} \to (0 < N - M \to N - M \in ℕ)$
105	104	adantl	$⊢ (L \in ℤ \land N - M \in ℕ_{0}) \to (0 < N - M \to N - M \in ℕ)$
106	102 105	syld	$⊢ (L \in ℤ \land N - M \in ℕ_{0}) \to ((0 < L \land L \leq N - M) \to N - M \in ℕ)$
107	106	exp4b	$⊢ L \in ℤ \to (N - M \in ℕ_{0} \to (0 < L \to (L \leq N - M \to N - M \in ℕ)))$
108	107	com23	$⊢ L \in ℤ \to (0 < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to N - M \in ℕ)))$
109	108	adantl	$⊢ (x + K \in ℤ \land L \in ℤ) \to (0 < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to N - M \in ℕ)))$
110	96 109	syld	$⊢ (x + K \in ℤ \land L \in ℤ) \to ((0 \leq x + K \land x + K < L) \to (N - M \in ℕ_{0} \to (L \leq N - M \to N - M \in ℕ)))$
111	110	expd	$⊢ (x + K \in ℤ \land L \in ℤ) \to (0 \leq x + K \to (x + K < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to N - M \in ℕ))))$
112	111	a1d	$⊢ (x + K \in ℤ \land L \in ℤ) \to ((x \in ℕ_{0} \land K \in ℕ_{0}) \to (0 \leq x + K \to (x + K < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to N - M \in ℕ)))))$
113	112	ex	$⊢ x + K \in ℤ \to (L \in ℤ \to ((x \in ℕ_{0} \land K \in ℕ_{0}) \to (0 \leq x + K \to (x + K < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to N - M \in ℕ))))))$
114	113	com24	$⊢ x + K \in ℤ \to (0 \leq x + K \to ((x \in ℕ_{0} \land K \in ℕ_{0}) \to (L \in ℤ \to (x + K < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to N - M \in ℕ))))))$
115	114	imp	$⊢ (x + K \in ℤ \land 0 \leq x + K) \to ((x \in ℕ_{0} \land K \in ℕ_{0}) \to (L \in ℤ \to (x + K < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to N - M \in ℕ)))))$
116	90 115	sylbi	$⊢ x + K \in ℕ_{0} \to ((x \in ℕ_{0} \land K \in ℕ_{0}) \to (L \in ℤ \to (x + K < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to N - M \in ℕ)))))$
117	85 116	mpcom	$⊢ (x \in ℕ_{0} \land K \in ℕ_{0}) \to (L \in ℤ \to (x + K < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to N - M \in ℕ))))$
118	117	impancom	$⊢ (x \in ℕ_{0} \land L \in ℤ) \to (K \in ℕ_{0} \to (x + K < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to N - M \in ℕ))))$
119	118	impcom	$⊢ (K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \to (x + K < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to N - M \in ℕ)))$
120	119	imp41	$⊢ ((((K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \land x + K < L) \land N - M \in ℕ_{0}) \land L \leq N - M) \to N - M \in ℕ$
121		nn0readdcl	$⊢ (x \in ℕ_{0} \land K \in ℕ_{0}) \to x + K \in ℝ$
122	121	ex	$⊢ x \in ℕ_{0} \to (K \in ℕ_{0} \to x + K \in ℝ)$
123	122	adantr	$⊢ (x \in ℕ_{0} \land L \in ℤ) \to (K \in ℕ_{0} \to x + K \in ℝ)$
124	123	impcom	$⊢ (K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \to x + K \in ℝ$
125		ltletr	$⊢ (x + K \in ℝ \land L \in ℝ \land N - M \in ℝ) \to ((x + K < L \land L \leq N - M) \to x + K < N - M)$
126	124 81 99 125	syl2an3an	$⊢ ((K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \land N - M \in ℕ_{0}) \to ((x + K < L \land L \leq N - M) \to x + K < N - M)$
127	126	exp4b	$⊢ (K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \to (N - M \in ℕ_{0} \to (x + K < L \to (L \leq N - M \to x + K < N - M)))$
128	127	com23	$⊢ (K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \to (x + K < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to x + K < N - M)))$
129	128	imp41	$⊢ ((((K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \land x + K < L) \land N - M \in ℕ_{0}) \land L \leq N - M) \to x + K < N - M$
130		elfzo0	$⊢ x + K \in (0 ..^N - M) \leftrightarrow (x + K \in ℕ_{0} \land N - M \in ℕ \land x + K < N - M)$
131	89 120 129 130	syl3anbrc	$⊢ ((((K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \land x + K < L) \land N - M \in ℕ_{0}) \land L \leq N - M) \to x + K \in (0 ..^N - M)$
132	131	exp41	$⊢ (K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \to (x + K < L \to (N - M \in ℕ_{0} \to (L \leq N - M \to x + K \in (0 ..^N - M))))$
133	84 132	sylbid	$⊢ (K \in ℕ_{0} \land (x \in ℕ_{0} \land L \in ℤ)) \to (x < L - K \to (N - M \in ℕ_{0} \to (L \leq N - M \to x + K \in (0 ..^N - M))))$
134	133	ex	$⊢ K \in ℕ_{0} \to ((x \in ℕ_{0} \land L \in ℤ) \to (x < L - K \to (N - M \in ℕ_{0} \to (L \leq N - M \to x + K \in (0 ..^N - M)))))$
135	134	com24	$⊢ K \in ℕ_{0} \to (N - M \in ℕ_{0} \to (x < L - K \to ((x \in ℕ_{0} \land L \in ℤ) \to (L \leq N - M \to x + K \in (0 ..^N - M)))))$
136	135	imp	$⊢ (K \in ℕ_{0} \land N - M \in ℕ_{0}) \to (x < L - K \to ((x \in ℕ_{0} \land L \in ℤ) \to (L \leq N - M \to x + K \in (0 ..^N - M))))$
137	136	com13	$⊢ (x \in ℕ_{0} \land L \in ℤ) \to (x < L - K \to ((K \in ℕ_{0} \land N - M \in ℕ_{0}) \to (L \leq N - M \to x + K \in (0 ..^N - M))))$
138	137	impancom	$⊢ (x \in ℕ_{0} \land x < L - K) \to (L \in ℤ \to ((K \in ℕ_{0} \land N - M \in ℕ_{0}) \to (L \leq N - M \to x + K \in (0 ..^N - M))))$
139	138	3adant2	$⊢ (x \in ℕ_{0} \land L - K \in ℕ \land x < L - K) \to (L \in ℤ \to ((K \in ℕ_{0} \land N - M \in ℕ_{0}) \to (L \leq N - M \to x + K \in (0 ..^N - M))))$
140	75 139	sylbi	$⊢ x \in (0 ..^L - K) \to (L \in ℤ \to ((K \in ℕ_{0} \land N - M \in ℕ_{0}) \to (L \leq N - M \to x + K \in (0 ..^N - M))))$
141	140	com14	$⊢ L \leq N - M \to (L \in ℤ \to ((K \in ℕ_{0} \land N - M \in ℕ_{0}) \to (x \in (0 ..^L - K) \to x + K \in (0 ..^N - M))))$
142	141	adantl	$⊢ (K \leq L \land L \leq N - M) \to (L \in ℤ \to ((K \in ℕ_{0} \land N - M \in ℕ_{0}) \to (x \in (0 ..^L - K) \to x + K \in (0 ..^N - M))))$
143	142	com12	$⊢ L \in ℤ \to ((K \leq L \land L \leq N - M) \to ((K \in ℕ_{0} \land N - M \in ℕ_{0}) \to (x \in (0 ..^L - K) \to x + K \in (0 ..^N - M))))$
144	143	3ad2ant3	$⊢ (K \in ℤ \land N - M \in ℤ \land L \in ℤ) \to ((K \leq L \land L \leq N - M) \to ((K \in ℕ_{0} \land N - M \in ℕ_{0}) \to (x \in (0 ..^L - K) \to x + K \in (0 ..^N - M))))$
145	144	imp	$⊢ ((K \in ℤ \land N - M \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N - M)) \to ((K \in ℕ_{0} \land N - M \in ℕ_{0}) \to (x \in (0 ..^L - K) \to x + K \in (0 ..^N - M)))$
146	74 145	sylbi	$⊢ L \in (K \dots N - M) \to ((K \in ℕ_{0} \land N - M \in ℕ_{0}) \to (x \in (0 ..^L - K) \to x + K \in (0 ..^N - M)))$
147	146	com12	$⊢ (K \in ℕ_{0} \land N - M \in ℕ_{0}) \to (L \in (K \dots N - M) \to (x \in (0 ..^L - K) \to x + K \in (0 ..^N - M)))$
148	147	3adant3	$⊢ (K \in ℕ_{0} \land N - M \in ℕ_{0} \land K \leq N - M) \to (L \in (K \dots N - M) \to (x \in (0 ..^L - K) \to x + K \in (0 ..^N - M)))$
149	73 148	sylbi	$⊢ K \in (0 \dots N - M) \to (L \in (K \dots N - M) \to (x \in (0 ..^L - K) \to x + K \in (0 ..^N - M)))$
150	149	imp	$⊢ (K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to (x \in (0 ..^L - K) \to x + K \in (0 ..^N - M))$
151	150	adantl	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (x \in (0 ..^L - K) \to x + K \in (0 ..^N - M))$
152	151	adantr	$⊢ (((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \to (x \in (0 ..^L - K) \to x + K \in (0 ..^N - M))$
153	152	imp	$⊢ ((((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \land x \in (0 ..^L - K)) \to x + K \in (0 ..^N - M)$
154		swrdfv	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x + K \in (0 ..^N - M)) \to (W substr ⟨M, N⟩) (x + K) = W (x + K + M)$
155	72 153 154	syl2anc	$⊢ ((((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \land x \in (0 ..^L - K)) \to (W substr ⟨M, N⟩) (x + K) = W (x + K + M)$
156	155	mpteq2dva	$⊢ (((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \to (x \in (0 ..^L - K) ⟼ (W substr ⟨M, N⟩) (x + K)) = (x \in (0 ..^L - K) ⟼ W (x + K + M))$
157	156	fveq1d	$⊢ (((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \to (x \in (0 ..^L - K) ⟼ (W substr ⟨M, N⟩) (x + K)) (y) = (x \in (0 ..^L - K) ⟼ W (x + K + M)) (y)$
158	25	adantr	$⊢ (((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \to (W \in Word V \land M + K \in (0 \dots M + L) \land M + L \in (0 \dots \|W\|))$
159	31 33 35	3anim123i	$⊢ (M \in ℤ \land L \in ℤ \land K \in ℤ) \to (M \in ℂ \land L \in ℂ \land K \in ℂ)$
160	159	3expa	$⊢ ((M \in ℤ \land L \in ℤ) \land K \in ℤ) \to (M \in ℂ \land L \in ℂ \land K \in ℂ)$
161	160 38	syl	$⊢ ((M \in ℤ \land L \in ℤ) \land K \in ℤ) \to L - K = M + L - (M + K)$
162	161	exp31	$⊢ M \in ℤ \to (L \in ℤ \to (K \in ℤ \to L - K = M + L - (M + K)))$
163	162	com3l	$⊢ L \in ℤ \to (K \in ℤ \to (M \in ℤ \to L - K = M + L - (M + K)))$
164	29 163	syl	$⊢ L \in (K \dots N - M) \to (K \in ℤ \to (M \in ℤ \to L - K = M + L - (M + K)))$
165	30 164	mpan9	$⊢ (K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to (M \in ℤ \to L - K = M + L - (M + K))$
166	28 165	syl5com	$⊢ M \in (0 \dots N) \to ((K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to L - K = M + L - (M + K))$
167	166	3ad2ant3	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to ((K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to L - K = M + L - (M + K))$
168	167	imp	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to L - K = M + L - (M + K)$
169	168	oveq2d	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (0 ..^L - K) = (0 ..^M + L - (M + K))$
170	169	eleq2d	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (y \in (0 ..^L - K) \leftrightarrow y \in (0 ..^M + L - (M + K)))$
171	170	biimpa	$⊢ (((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \to y \in (0 ..^M + L - (M + K))$
172		swrdfv	$⊢ ((W \in Word V \land M + K \in (0 \dots M + L) \land M + L \in (0 \dots \|W\|)) \land y \in (0 ..^M + L - (M + K))) \to (W substr ⟨M + K, M + L⟩) (y) = W (y + M + K)$
173	158 171 172	syl2anc	$⊢ (((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \to (W substr ⟨M + K, M + L⟩) (y) = W (y + M + K)$
174	71 157 173	3eqtr4d	$⊢ (((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \land y \in (0 ..^L - K)) \to (x \in (0 ..^L - K) ⟼ (W substr ⟨M, N⟩) (x + K)) (y) = (W substr ⟨M + K, M + L⟩) (y)$
175	24 47 174	eqfnfvd	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (x \in (0 ..^L - K) ⟼ (W substr ⟨M, N⟩) (x + K)) = W substr ⟨M + K, M + L⟩$
176	20 175	eqtrd	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (W substr ⟨M, N⟩) substr ⟨K, L⟩ = W substr ⟨M + K, M + L⟩$
177	176	ex	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to ((K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to (W substr ⟨M, N⟩) substr ⟨K, L⟩ = W substr ⟨M + K, M + L⟩)$

Metamath Proof Explorer

Theorem swrdswrd

Proof