pfxccatpfx1

Description: A prefix of a concatenation being a prefix of the first concatenated word. (Contributed by AV, 10-May-2020)

		Ref	Expression
	Hypothesis	swrdccatin2.l	$⊢ L = \|A\|$
	Assertion	pfxccatpfx1	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots L)) \to (A ++ B) prefix N = A prefix N$

Proof

Step	Hyp	Ref	Expression
1		swrdccatin2.l	$⊢ L = \|A\|$
2		3simpa	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots L)) \to (A \in Word V \land B \in Word V)$
3		elfznn0	$⊢ N \in (0 \dots L) \to N \in ℕ_{0}$
4		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
5	3 4	syl	$⊢ N \in (0 \dots L) \to 0 \in (0 \dots N)$
6	1	oveq2i	$⊢ (0 \dots L) = (0 \dots \|A\|)$
7	6	eleq2i	$⊢ N \in (0 \dots L) \leftrightarrow N \in (0 \dots \|A\|)$
8	7	biimpi	$⊢ N \in (0 \dots L) \to N \in (0 \dots \|A\|)$
9	5 8	jca	$⊢ N \in (0 \dots L) \to (0 \in (0 \dots N) \land N \in (0 \dots \|A\|))$
10	9	3ad2ant3	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots L)) \to (0 \in (0 \dots N) \land N \in (0 \dots \|A\|))$
11		swrdccatin1	$⊢ (A \in Word V \land B \in Word V) \to ((0 \in (0 \dots N) \land N \in (0 \dots \|A\|)) \to (A ++ B) substr ⟨0, N⟩ = A substr ⟨0, N⟩)$
12	2 10 11	sylc	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots L)) \to (A ++ B) substr ⟨0, N⟩ = A substr ⟨0, N⟩$
13		ccatcl	$⊢ (A \in Word V \land B \in Word V) \to A ++ B \in Word V$
14	13	3adant3	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots L)) \to A ++ B \in Word V$
15	3	3ad2ant3	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots L)) \to N \in ℕ_{0}$
16	14 15	jca	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots L)) \to (A ++ B \in Word V \land N \in ℕ_{0})$
17		pfxval	$⊢ (A ++ B \in Word V \land N \in ℕ_{0}) \to (A ++ B) prefix N = (A ++ B) substr ⟨0, N⟩$
18	16 17	syl	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots L)) \to (A ++ B) prefix N = (A ++ B) substr ⟨0, N⟩$
19		pfxval	$⊢ (A \in Word V \land N \in ℕ_{0}) \to A prefix N = A substr ⟨0, N⟩$
20	3 19	sylan2	$⊢ (A \in Word V \land N \in (0 \dots L)) \to A prefix N = A substr ⟨0, N⟩$
21	20	3adant2	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots L)) \to A prefix N = A substr ⟨0, N⟩$
22	12 18 21	3eqtr4d	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots L)) \to (A ++ B) prefix N = A prefix N$

Metamath Proof Explorer

Theorem pfxccatpfx1

Proof