pfxccatin12

Description: The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 5-Apr-2018) (Revised by AV, 9-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		swrdccatin2.l	$⊢ L = \|A\|$
2	1	pfxccatin12lem2c	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \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\|))$
3		swrdvalfn	$⊢ (A ++ 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)$
4	2 3	syl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to ((A ++ B) substr ⟨M, N⟩) Fn (0 ..^N - M)$
5		swrdcl	$⊢ A \in Word V \to A substr ⟨M, L⟩ \in Word V$
6		pfxcl	$⊢ B \in Word V \to B prefix (N - L) \in Word V$
7		ccatvalfn	$⊢ (A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V) \to ((A substr ⟨M, L⟩) ++ (B prefix (N - L))) Fn (0 ..^\|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|)$
8	5 6 7	syl2an	$⊢ (A \in Word V \land B \in Word V) \to ((A substr ⟨M, L⟩) ++ (B prefix (N - L))) Fn (0 ..^\|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|)$
9	8	adantr	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to ((A substr ⟨M, L⟩) ++ (B prefix (N - L))) Fn (0 ..^\|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|)$
10		simpll	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to A \in Word V$
11		simprl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to M \in (0 \dots L)$
12		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
13		nn0fz0	$⊢ \|A\| \in ℕ_{0} \leftrightarrow \|A\| \in (0 \dots \|A\|)$
14	12 13	sylib	$⊢ A \in Word V \to \|A\| \in (0 \dots \|A\|)$
15	1 14	eqeltrid	$⊢ A \in Word V \to L \in (0 \dots \|A\|)$
16	15	ad2antrr	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to L \in (0 \dots \|A\|)$
17		swrdlen	$⊢ (A \in Word V \land M \in (0 \dots L) \land L \in (0 \dots \|A\|)) \to \|A substr ⟨M, L⟩\| = L - M$
18	10 11 16 17	syl3anc	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to \|A substr ⟨M, L⟩\| = L - M$
19		lencl	$⊢ B \in Word V \to \|B\| \in ℕ_{0}$
20	19	nn0zd	$⊢ B \in Word V \to \|B\| \in ℤ$
21		elfzmlbp	$⊢ (\|B\| \in ℤ \land N \in (L \dots L + \|B\|)) \to N - L \in (0 \dots \|B\|)$
22	20 21	sylan	$⊢ (B \in Word V \land N \in (L \dots L + \|B\|)) \to N - L \in (0 \dots \|B\|)$
23		pfxlen	$⊢ (B \in Word V \land N - L \in (0 \dots \|B\|)) \to \|B prefix (N - L)\| = N - L$
24	22 23	syldan	$⊢ (B \in Word V \land N \in (L \dots L + \|B\|)) \to \|B prefix (N - L)\| = N - L$
25	24	ad2ant2l	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to \|B prefix (N - L)\| = N - L$
26	18 25	oveq12d	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to \|A substr ⟨M, L⟩\| + \|B prefix (N - L)\| = (L - M) + N - L$
27		elfz2nn0	$⊢ M \in (0 \dots L) \leftrightarrow (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L)$
28		nn0cn	$⊢ L \in ℕ_{0} \to L \in ℂ$
29	28	ad2antll	$⊢ (N \in ℤ \land (M \in ℕ_{0} \land L \in ℕ_{0})) \to L \in ℂ$
30		nn0cn	$⊢ M \in ℕ_{0} \to M \in ℂ$
31	30	ad2antrl	$⊢ (N \in ℤ \land (M \in ℕ_{0} \land L \in ℕ_{0})) \to M \in ℂ$
32		zcn	$⊢ N \in ℤ \to N \in ℂ$
33	32	adantr	$⊢ (N \in ℤ \land (M \in ℕ_{0} \land L \in ℕ_{0})) \to N \in ℂ$
34	29 31 33	3jca	$⊢ (N \in ℤ \land (M \in ℕ_{0} \land L \in ℕ_{0})) \to (L \in ℂ \land M \in ℂ \land N \in ℂ)$
35	34	ex	$⊢ N \in ℤ \to ((M \in ℕ_{0} \land L \in ℕ_{0}) \to (L \in ℂ \land M \in ℂ \land N \in ℂ))$
36		elfzelz	$⊢ N \in (L \dots L + \|B\|) \to N \in ℤ$
37	35 36	syl11	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (N \in (L \dots L + \|B\|) \to (L \in ℂ \land M \in ℂ \land N \in ℂ))$
38	37	3adant3	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (N \in (L \dots L + \|B\|) \to (L \in ℂ \land M \in ℂ \land N \in ℂ))$
39	27 38	sylbi	$⊢ M \in (0 \dots L) \to (N \in (L \dots L + \|B\|) \to (L \in ℂ \land M \in ℂ \land N \in ℂ))$
40	39	imp	$⊢ (M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to (L \in ℂ \land M \in ℂ \land N \in ℂ)$
41		npncan3	$⊢ (L \in ℂ \land M \in ℂ \land N \in ℂ) \to (L - M) + N - L = N - M$
42	40 41	syl	$⊢ (M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to (L - M) + N - L = N - M$
43	42	adantl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (L - M) + N - L = N - M$
44	26 43	eqtr2d	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to N - M = \|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|$
45	44	oveq2d	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (0 ..^N - M) = (0 ..^\|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|)$
46	45	fneq2d	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (((A substr ⟨M, L⟩) ++ (B prefix (N - L))) Fn (0 ..^N - M) \leftrightarrow ((A substr ⟨M, L⟩) ++ (B prefix (N - L))) Fn (0 ..^\|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|))$
47	9 46	mpbird	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to ((A substr ⟨M, L⟩) ++ (B prefix (N - L))) Fn (0 ..^N - M)$
48		simprl	$⊢ (k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|)))$
49		simpr	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M)) \to k \in (0 ..^N - M)$
50	49	anim2i	$⊢ (k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to (k \in (0 ..^L - M) \land k \in (0 ..^N - M))$
51	50	ancomd	$⊢ (k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to (k \in (0 ..^N - M) \land k \in (0 ..^L - M))$
52	1	pfxccatin12lem3	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to ((k \in (0 ..^N - M) \land k \in (0 ..^L - M)) \to ((A ++ B) substr ⟨M, N⟩) (k) = (A substr ⟨M, L⟩) (k))$
53	48 51 52	sylc	$⊢ (k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to ((A ++ B) substr ⟨M, N⟩) (k) = (A substr ⟨M, L⟩) (k)$
54	5 6	anim12i	$⊢ (A \in Word V \land B \in Word V) \to (A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V)$
55	54	adantr	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V)$
56	55	ad2antrl	$⊢ (k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to (A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V)$
57		simpl	$⊢ (k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to k \in (0 ..^L - M)$
58	18	oveq2d	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (0 ..^\|A substr ⟨M, L⟩\|) = (0 ..^L - M)$
59	58	ad2antrl	$⊢ (k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to (0 ..^\|A substr ⟨M, L⟩\|) = (0 ..^L - M)$
60	57 59	eleqtrrd	$⊢ (k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to k \in (0 ..^\|A substr ⟨M, L⟩\|)$
61		df-3an	$⊢ (A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V \land k \in (0 ..^\|A substr ⟨M, L⟩\|)) \leftrightarrow ((A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V) \land k \in (0 ..^\|A substr ⟨M, L⟩\|))$
62	56 60 61	sylanbrc	$⊢ (k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to (A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V \land k \in (0 ..^\|A substr ⟨M, L⟩\|))$
63		ccatval1	$⊢ (A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V \land k \in (0 ..^\|A substr ⟨M, L⟩\|)) \to ((A substr ⟨M, L⟩) ++ (B prefix (N - L))) (k) = (A substr ⟨M, L⟩) (k)$
64	62 63	syl	$⊢ (k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to ((A substr ⟨M, L⟩) ++ (B prefix (N - L))) (k) = (A substr ⟨M, L⟩) (k)$
65	53 64	eqtr4d	$⊢ (k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to ((A ++ B) substr ⟨M, N⟩) (k) = ((A substr ⟨M, L⟩) ++ (B prefix (N - L))) (k)$
66		simprl	$⊢ (\neg k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|)))$
67	49	anim2i	$⊢ (\neg k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to (\neg k \in (0 ..^L - M) \land k \in (0 ..^N - M))$
68	67	ancomd	$⊢ (\neg k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to (k \in (0 ..^N - M) \land \neg k \in (0 ..^L - M))$
69	1	pfxccatin12lem2	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to ((k \in (0 ..^N - M) \land \neg k \in (0 ..^L - M)) \to ((A ++ B) substr ⟨M, N⟩) (k) = (B prefix (N - L)) (k - \|A substr ⟨M, L⟩\|))$
70	66 68 69	sylc	$⊢ (\neg k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to ((A ++ B) substr ⟨M, N⟩) (k) = (B prefix (N - L)) (k - \|A substr ⟨M, L⟩\|)$
71	55	ad2antrl	$⊢ (\neg k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to (A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V)$
72		elfzuz	$⊢ N \in (L \dots L + \|B\|) \to N \in ℤ_{\geq L}$
73		eluzelz	$⊢ N \in ℤ_{\geq L} \to N \in ℤ$
74		id	$⊢ (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ) \to (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ)$
75	74	3expia	$⊢ (L \in ℕ_{0} \land M \in ℕ_{0}) \to (N \in ℤ \to (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ))$
76	75	ancoms	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (N \in ℤ \to (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ))$
77	76	3adant3	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (N \in ℤ \to (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ))$
78	27 77	sylbi	$⊢ M \in (0 \dots L) \to (N \in ℤ \to (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ))$
79	73 78	syl5com	$⊢ N \in ℤ_{\geq L} \to (M \in (0 \dots L) \to (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ))$
80	72 79	syl	$⊢ N \in (L \dots L + \|B\|) \to (M \in (0 \dots L) \to (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ))$
81	80	impcom	$⊢ (M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ)$
82	81	adantl	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ)$
83	82	ad2antrl	$⊢ (\neg k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ)$
84		pfxccatin12lem4	$⊢ (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ) \to ((k \in (0 ..^N - M) \land \neg k \in (0 ..^L - M)) \to k \in (L - M ..^(L - M) + N - L))$
85	83 68 84	sylc	$⊢ (\neg k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to k \in (L - M ..^(L - M) + N - L)$
86	18 26	oveq12d	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (\|A substr ⟨M, L⟩\| ..^\|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|) = (L - M ..^(L - M) + N - L)$
87	86	ad2antrl	$⊢ (\neg k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to (\|A substr ⟨M, L⟩\| ..^\|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|) = (L - M ..^(L - M) + N - L)$
88	85 87	eleqtrrd	$⊢ (\neg k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to k \in (\|A substr ⟨M, L⟩\| ..^\|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|)$
89		df-3an	$⊢ (A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V \land k \in (\|A substr ⟨M, L⟩\| ..^\|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|)) \leftrightarrow ((A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V) \land k \in (\|A substr ⟨M, L⟩\| ..^\|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|))$
90	71 88 89	sylanbrc	$⊢ (\neg k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to (A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V \land k \in (\|A substr ⟨M, L⟩\| ..^\|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|))$
91		ccatval2	$⊢ (A substr ⟨M, L⟩ \in Word V \land B prefix (N - L) \in Word V \land k \in (\|A substr ⟨M, L⟩\| ..^\|A substr ⟨M, L⟩\| + \|B prefix (N - L)\|)) \to ((A substr ⟨M, L⟩) ++ (B prefix (N - L))) (k) = (B prefix (N - L)) (k - \|A substr ⟨M, L⟩\|)$
92	90 91	syl	$⊢ (\neg k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to ((A substr ⟨M, L⟩) ++ (B prefix (N - L))) (k) = (B prefix (N - L)) (k - \|A substr ⟨M, L⟩\|)$
93	70 92	eqtr4d	$⊢ (\neg k \in (0 ..^L - M) \land (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M))) \to ((A ++ B) substr ⟨M, N⟩) (k) = ((A substr ⟨M, L⟩) ++ (B prefix (N - L))) (k)$
94	65 93	pm2.61ian	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land k \in (0 ..^N - M)) \to ((A ++ B) substr ⟨M, N⟩) (k) = ((A substr ⟨M, L⟩) ++ (B prefix (N - L))) (k)$
95	4 47 94	eqfnfvd	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (A ++ B) substr ⟨M, N⟩ = (A substr ⟨M, L⟩) ++ (B prefix (N - L))$
96	95	ex	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to (A ++ B) substr ⟨M, N⟩ = (A substr ⟨M, L⟩) ++ (B prefix (N - L)))$

Metamath Proof Explorer

Theorem pfxccatin12

Proof