swrdccatin2d

Description: The subword of a concatenation of two words within the second of the concatenated words. (Contributed by AV, 31-May-2018) (Revised by Mario Carneiro/AV, 21-Oct-2018)

	Ref	Expression
Hypotheses	swrdccatind.l	$⊢ φ \to \|A\| = L$
	swrdccatind.w	$⊢ φ \to (A \in Word V \land B \in Word V)$
	swrdccatin2d.1	$⊢ φ \to M \in (L \dots N)$
	swrdccatin2d.2	$⊢ φ \to N \in (L \dots L + \|B\|)$
Assertion	swrdccatin2d	$⊢ φ \to (A ++ B) substr ⟨M, N⟩ = B substr ⟨M - L, N - L⟩$

Proof

Step	Hyp	Ref	Expression
1		swrdccatind.l	$⊢ φ \to \|A\| = L$
2		swrdccatind.w	$⊢ φ \to (A \in Word V \land B \in Word V)$
3		swrdccatin2d.1	$⊢ φ \to M \in (L \dots N)$
4		swrdccatin2d.2	$⊢ φ \to N \in (L \dots L + \|B\|)$
5	2	adantl	$⊢ (\|A\| = L \land φ) \to (A \in Word V \land B \in Word V)$
6	3 4	jca	$⊢ φ \to (M \in (L \dots N) \land N \in (L \dots L + \|B\|))$
7	6	adantl	$⊢ (\|A\| = L \land φ) \to (M \in (L \dots N) \land N \in (L \dots L + \|B\|))$
8		oveq1	$⊢ \|A\| = L \to (\|A\| \dots N) = (L \dots N)$
9	8	eleq2d	$⊢ \|A\| = L \to (M \in (\|A\| \dots N) \leftrightarrow M \in (L \dots N))$
10		id	$⊢ \|A\| = L \to \|A\| = L$
11		oveq1	$⊢ \|A\| = L \to \|A\| + \|B\| = L + \|B\|$
12	10 11	oveq12d	$⊢ \|A\| = L \to (\|A\| \dots \|A\| + \|B\|) = (L \dots L + \|B\|)$
13	12	eleq2d	$⊢ \|A\| = L \to (N \in (\|A\| \dots \|A\| + \|B\|) \leftrightarrow N \in (L \dots L + \|B\|))$
14	9 13	anbi12d	$⊢ \|A\| = L \to ((M \in (\|A\| \dots N) \land N \in (\|A\| \dots \|A\| + \|B\|)) \leftrightarrow (M \in (L \dots N) \land N \in (L \dots L + \|B\|)))$
15	14	adantr	$⊢ (\|A\| = L \land φ) \to ((M \in (\|A\| \dots N) \land N \in (\|A\| \dots \|A\| + \|B\|)) \leftrightarrow (M \in (L \dots N) \land N \in (L \dots L + \|B\|)))$
16	7 15	mpbird	$⊢ (\|A\| = L \land φ) \to (M \in (\|A\| \dots N) \land N \in (\|A\| \dots \|A\| + \|B\|))$
17	5 16	jca	$⊢ (\|A\| = L \land φ) \to ((A \in Word V \land B \in Word V) \land (M \in (\|A\| \dots N) \land N \in (\|A\| \dots \|A\| + \|B\|)))$
18	17	ex	$⊢ \|A\| = L \to (φ \to ((A \in Word V \land B \in Word V) \land (M \in (\|A\| \dots N) \land N \in (\|A\| \dots \|A\| + \|B\|))))$
19		eqid	$⊢ \|A\| = \|A\|$
20	19	swrdccatin2	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (\|A\| \dots N) \land N \in (\|A\| \dots \|A\| + \|B\|)) \to (A ++ B) substr ⟨M, N⟩ = B substr ⟨M - \|A\|, N - \|A\|⟩)$
21	20	imp	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (\|A\| \dots N) \land N \in (\|A\| \dots \|A\| + \|B\|))) \to (A ++ B) substr ⟨M, N⟩ = B substr ⟨M - \|A\|, N - \|A\|⟩$
22	18 21	syl6	$⊢ \|A\| = L \to (φ \to (A ++ B) substr ⟨M, N⟩ = B substr ⟨M - \|A\|, N - \|A\|⟩)$
23		oveq2	$⊢ \|A\| = L \to M - \|A\| = M - L$
24		oveq2	$⊢ \|A\| = L \to N - \|A\| = N - L$
25	23 24	opeq12d	$⊢ \|A\| = L \to ⟨M - \|A\|, N - \|A\|⟩ = ⟨M - L, N - L⟩$
26	25	oveq2d	$⊢ \|A\| = L \to B substr ⟨M - \|A\|, N - \|A\|⟩ = B substr ⟨M - L, N - L⟩$
27	26	eqeq2d	$⊢ \|A\| = L \to ((A ++ B) substr ⟨M, N⟩ = B substr ⟨M - \|A\|, N - \|A\|⟩ \leftrightarrow (A ++ B) substr ⟨M, N⟩ = B substr ⟨M - L, N - L⟩)$
28	22 27	sylibd	$⊢ \|A\| = L \to (φ \to (A ++ B) substr ⟨M, N⟩ = B substr ⟨M - L, N - L⟩)$
29	1 28	mpcom	$⊢ φ \to (A ++ B) substr ⟨M, N⟩ = B substr ⟨M - L, N - L⟩$

Metamath Proof Explorer

Theorem swrdccatin2d

Proof