This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem swrdccatin1d

Description: The subword of a concatenation of two words within the first 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)$
		swrdccatin1d.1	$⊢ φ \to M \in (0 \dots N)$
		swrdccatin1d.2	$⊢ φ \to N \in (0 \dots L)$
	Assertion	swrdccatin1d	$⊢ φ \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩$

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		swrdccatin1d.1	$⊢ φ \to M \in (0 \dots N)$
4		swrdccatin1d.2	$⊢ φ \to N \in (0 \dots L)$
5		oveq2	$⊢ \|A\| = L \to (0 \dots \|A\|) = (0 \dots L)$
6	5	eleq2d	$⊢ \|A\| = L \to (N \in (0 \dots \|A\|) \leftrightarrow N \in (0 \dots L))$
7	4 6	imbitrrid	$⊢ \|A\| = L \to (φ \to N \in (0 \dots \|A\|))$
8	1 7	mpcom	$⊢ φ \to N \in (0 \dots \|A\|)$
9	3 8	jca	$⊢ φ \to (M \in (0 \dots N) \land N \in (0 \dots \|A\|))$
10		swrdccatin1	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩)$
11	2 9 10	sylc	$⊢ φ \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩$