pfxpfx

Description: A prefix of a prefix is a prefix. (Contributed by Alexander van der Vekens, 7-Apr-2018) (Revised by AV, 8-May-2020)

		Ref	Expression
	Assertion	pfxpfx	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to (W prefix N) prefix L = W prefix L$

Proof

Step	Hyp	Ref	Expression
1		elfznn0	$⊢ N \in (0 \dots \|W\|) \to N \in ℕ_{0}$
2	1	anim2i	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to (W \in Word V \land N \in ℕ_{0})$
3	2	3adant3	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to (W \in Word V \land N \in ℕ_{0})$
4		pfxval	$⊢ (W \in Word V \land N \in ℕ_{0}) \to W prefix N = W substr ⟨0, N⟩$
5	3 4	syl	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to W prefix N = W substr ⟨0, N⟩$
6	5	oveq1d	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to (W prefix N) prefix L = (W substr ⟨0, N⟩) prefix L$
7		simp1	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to W \in Word V$
8		simp2	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to N \in (0 \dots \|W\|)$
9		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
10	1 9	syl	$⊢ N \in (0 \dots \|W\|) \to 0 \in (0 \dots N)$
11	10	3ad2ant2	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to 0 \in (0 \dots N)$
12	7 8 11	3jca	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to (W \in Word V \land N \in (0 \dots \|W\|) \land 0 \in (0 \dots N))$
13	1	nn0cnd	$⊢ N \in (0 \dots \|W\|) \to N \in ℂ$
14	13	subid1d	$⊢ N \in (0 \dots \|W\|) \to N - 0 = N$
15	14	eqcomd	$⊢ N \in (0 \dots \|W\|) \to N = N - 0$
16	15	adantl	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to N = N - 0$
17	16	oveq2d	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to (0 \dots N) = (0 \dots N - 0)$
18	17	eleq2d	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to (L \in (0 \dots N) \leftrightarrow L \in (0 \dots N - 0))$
19	18	biimp3a	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to L \in (0 \dots N - 0)$
20		pfxswrd	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land 0 \in (0 \dots N)) \to (L \in (0 \dots N - 0) \to (W substr ⟨0, N⟩) prefix L = W substr ⟨0, 0 + L⟩)$
21	12 19 20	sylc	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to (W substr ⟨0, N⟩) prefix L = W substr ⟨0, 0 + L⟩$
22		elfznn0	$⊢ L \in (0 \dots N) \to L \in ℕ_{0}$
23	22	nn0cnd	$⊢ L \in (0 \dots N) \to L \in ℂ$
24	23	addid2d	$⊢ L \in (0 \dots N) \to 0 + L = L$
25	24	opeq2d	$⊢ L \in (0 \dots N) \to ⟨0, 0 + L⟩ = ⟨0, L⟩$
26	25	oveq2d	$⊢ L \in (0 \dots N) \to W substr ⟨0, 0 + L⟩ = W substr ⟨0, L⟩$
27	26	3ad2ant3	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to W substr ⟨0, 0 + L⟩ = W substr ⟨0, L⟩$
28	22	anim2i	$⊢ (W \in Word V \land L \in (0 \dots N)) \to (W \in Word V \land L \in ℕ_{0})$
29	28	3adant2	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to (W \in Word V \land L \in ℕ_{0})$
30		pfxval	$⊢ (W \in Word V \land L \in ℕ_{0}) \to W prefix L = W substr ⟨0, L⟩$
31	29 30	syl	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to W prefix L = W substr ⟨0, L⟩$
32	27 31	eqtr4d	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to W substr ⟨0, 0 + L⟩ = W prefix L$
33	6 21 32	3eqtrd	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land L \in (0 \dots N)) \to (W prefix N) prefix L = W prefix L$

Metamath Proof Explorer

Theorem pfxpfx

Proof