pfxccatin12d

Description: The subword of a concatenation of two words within both of the concatenated words. (Contributed by AV, 31-May-2018) (Revised by AV, 10-May-2020)

	Ref	Expression
Hypotheses	swrdccatind.l	$⊢ φ \to \|A\| = L$
	swrdccatind.w	$⊢ φ \to (A \in Word V \land B \in Word V)$
	pfxccatin12d.m	$⊢ φ \to M \in (0 \dots L)$
	pfxccatin12d.n	$⊢ φ \to N \in (L \dots L + \|B\|)$
Assertion	pfxccatin12d	$⊢ φ \to (A ++ B) substr ⟨M, N⟩ = (A substr ⟨M, L⟩) ++ (B prefix (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		pfxccatin12d.m	$⊢ φ \to M \in (0 \dots L)$
4		pfxccatin12d.n	$⊢ φ \to N \in (L \dots L + \|B\|)$
5	1	oveq2d	$⊢ φ \to (0 \dots \|A\|) = (0 \dots L)$
6	5	eleq2d	$⊢ φ \to (M \in (0 \dots \|A\|) \leftrightarrow M \in (0 \dots L))$
7	1	oveq1d	$⊢ φ \to \|A\| + \|B\| = L + \|B\|$
8	1 7	oveq12d	$⊢ φ \to (\|A\| \dots \|A\| + \|B\|) = (L \dots L + \|B\|)$
9	8	eleq2d	$⊢ φ \to (N \in (\|A\| \dots \|A\| + \|B\|) \leftrightarrow N \in (L \dots L + \|B\|))$
10	6 9	anbi12d	$⊢ φ \to ((M \in (0 \dots \|A\|) \land N \in (\|A\| \dots \|A\| + \|B\|)) \leftrightarrow (M \in (0 \dots L) \land N \in (L \dots L + \|B\|)))$
11	3 4 10	mpbir2and	$⊢ φ \to (M \in (0 \dots \|A\|) \land N \in (\|A\| \dots \|A\| + \|B\|))$
12		eqid	$⊢ \|A\| = \|A\|$
13	12	pfxccatin12	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots \|A\|) \land N \in (\|A\| \dots \|A\| + \|B\|)) \to (A ++ B) substr ⟨M, N⟩ = (A substr ⟨M, \|A\|⟩) ++ (B prefix (N - \|A\|)))$
14	2 11 13	sylc	$⊢ φ \to (A ++ B) substr ⟨M, N⟩ = (A substr ⟨M, \|A\|⟩) ++ (B prefix (N - \|A\|))$
15	1	opeq2d	$⊢ φ \to ⟨M, \|A\|⟩ = ⟨M, L⟩$
16	15	oveq2d	$⊢ φ \to A substr ⟨M, \|A\|⟩ = A substr ⟨M, L⟩$
17	1	oveq2d	$⊢ φ \to N - \|A\| = N - L$
18	17	oveq2d	$⊢ φ \to B prefix (N - \|A\|) = B prefix (N - L)$
19	16 18	oveq12d	$⊢ φ \to (A substr ⟨M, \|A\|⟩) ++ (B prefix (N - \|A\|)) = (A substr ⟨M, L⟩) ++ (B prefix (N - L))$
20	14 19	eqtrd	$⊢ φ \to (A ++ B) substr ⟨M, N⟩ = (A substr ⟨M, L⟩) ++ (B prefix (N - L))$

Metamath Proof Explorer

Theorem pfxccatin12d

Proof