pfxswrd

Description: A prefix of a subword is a subword. (Contributed by AV, 2-Apr-2018) (Revised by AV, 8-May-2020)

		Ref	Expression
	Assertion	pfxswrd	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (L \in (0 \dots N - M) \to (W substr ⟨M, N⟩) prefix L = W substr ⟨M, M + L⟩)$

Proof

Step	Hyp	Ref	Expression
1		ovexd	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to W substr ⟨M, N⟩ \in V$
2		elfznn0	$⊢ L \in (0 \dots N - M) \to L \in ℕ_{0}$
3		pfxval	$⊢ (W substr ⟨M, N⟩ \in V \land L \in ℕ_{0}) \to (W substr ⟨M, N⟩) prefix L = (W substr ⟨M, N⟩) substr ⟨0, L⟩$
4	1 2 3	syl2an	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land L \in (0 \dots N - M)) \to (W substr ⟨M, N⟩) prefix L = (W substr ⟨M, N⟩) substr ⟨0, L⟩$
5		fznn0sub	$⊢ M \in (0 \dots N) \to N - M \in ℕ_{0}$
6	5	3ad2ant3	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to N - M \in ℕ_{0}$
7		0elfz	$⊢ N - M \in ℕ_{0} \to 0 \in (0 \dots N - M)$
8	6 7	syl	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to 0 \in (0 \dots N - M)$
9	8	anim1i	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land L \in (0 \dots N - M)) \to (0 \in (0 \dots N - M) \land L \in (0 \dots N - M))$
10		swrdswrd	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to ((0 \in (0 \dots N - M) \land L \in (0 \dots N - M)) \to (W substr ⟨M, N⟩) substr ⟨0, L⟩ = W substr ⟨M + 0, M + L⟩)$
11	10	imp	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (0 \in (0 \dots N - M) \land L \in (0 \dots N - M))) \to (W substr ⟨M, N⟩) substr ⟨0, L⟩ = W substr ⟨M + 0, M + L⟩$
12	9 11	syldan	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land L \in (0 \dots N - M)) \to (W substr ⟨M, N⟩) substr ⟨0, L⟩ = W substr ⟨M + 0, M + L⟩$
13		elfznn0	$⊢ M \in (0 \dots N) \to M \in ℕ_{0}$
14		nn0cn	$⊢ M \in ℕ_{0} \to M \in ℂ$
15	14	addid1d	$⊢ M \in ℕ_{0} \to M + 0 = M$
16	13 15	syl	$⊢ M \in (0 \dots N) \to M + 0 = M$
17	16	3ad2ant3	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to M + 0 = M$
18	17	adantr	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land L \in (0 \dots N - M)) \to M + 0 = M$
19	18	opeq1d	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land L \in (0 \dots N - M)) \to ⟨M + 0, M + L⟩ = ⟨M, M + L⟩$
20	19	oveq2d	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land L \in (0 \dots N - M)) \to W substr ⟨M + 0, M + L⟩ = W substr ⟨M, M + L⟩$
21	4 12 20	3eqtrd	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land L \in (0 \dots N - M)) \to (W substr ⟨M, N⟩) prefix L = W substr ⟨M, M + L⟩$
22	21	ex	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (L \in (0 \dots N - M) \to (W substr ⟨M, N⟩) prefix L = W substr ⟨M, M + L⟩)$

Metamath Proof Explorer

Theorem pfxswrd

Proof