swrdpfx

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

		Ref	Expression
	Assertion	swrdpfx	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to ((K \in (0 \dots N) \land L \in (K \dots N)) \to (W prefix N) substr ⟨K, L⟩ = W substr ⟨K, 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	adantr	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|)) \land (K \in (0 \dots N) \land L \in (K \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 (K \in (0 \dots N) \land L \in (K \dots N))) \to W prefix N = W substr ⟨0, N⟩$
6	5	oveq1d	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|)) \land (K \in (0 \dots N) \land L \in (K \dots N))) \to (W prefix N) substr ⟨K, L⟩ = (W substr ⟨0, N⟩) substr ⟨K, L⟩$
7		simpl	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to W \in Word V$
8		simpr	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \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	adantl	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to 0 \in (0 \dots N)$
12	7 8 11	3jca	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to (W \in Word V \land N \in (0 \dots \|W\|) \land 0 \in (0 \dots N))$
13	12	adantr	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|)) \land (K \in (0 \dots N) \land L \in (K \dots N))) \to (W \in Word V \land N \in (0 \dots \|W\|) \land 0 \in (0 \dots N))$
14		elfzelz	$⊢ N \in (0 \dots \|W\|) \to N \in ℤ$
15		zcn	$⊢ N \in ℤ \to N \in ℂ$
16	15	subid1d	$⊢ N \in ℤ \to N - 0 = N$
17	16	eqcomd	$⊢ N \in ℤ \to N = N - 0$
18	14 17	syl	$⊢ N \in (0 \dots \|W\|) \to N = N - 0$
19	18	adantl	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to N = N - 0$
20	19	oveq2d	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to (0 \dots N) = (0 \dots N - 0)$
21	20	eleq2d	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to (K \in (0 \dots N) \leftrightarrow K \in (0 \dots N - 0))$
22	19	oveq2d	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to (K \dots N) = (K \dots N - 0)$
23	22	eleq2d	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to (L \in (K \dots N) \leftrightarrow L \in (K \dots N - 0))$
24	21 23	anbi12d	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to ((K \in (0 \dots N) \land L \in (K \dots N)) \leftrightarrow (K \in (0 \dots N - 0) \land L \in (K \dots N - 0)))$
25	24	biimpa	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|)) \land (K \in (0 \dots N) \land L \in (K \dots N))) \to (K \in (0 \dots N - 0) \land L \in (K \dots N - 0))$
26		swrdswrd	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land 0 \in (0 \dots N)) \to ((K \in (0 \dots N - 0) \land L \in (K \dots N - 0)) \to (W substr ⟨0, N⟩) substr ⟨K, L⟩ = W substr ⟨0 + K, 0 + L⟩)$
27	13 25 26	sylc	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|)) \land (K \in (0 \dots N) \land L \in (K \dots N))) \to (W substr ⟨0, N⟩) substr ⟨K, L⟩ = W substr ⟨0 + K, 0 + L⟩$
28		elfzelz	$⊢ K \in (0 \dots N) \to K \in ℤ$
29	28	zcnd	$⊢ K \in (0 \dots N) \to K \in ℂ$
30	29	adantr	$⊢ (K \in (0 \dots N) \land L \in (K \dots N)) \to K \in ℂ$
31	30	adantl	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|)) \land (K \in (0 \dots N) \land L \in (K \dots N))) \to K \in ℂ$
32	31	addid2d	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|)) \land (K \in (0 \dots N) \land L \in (K \dots N))) \to 0 + K = K$
33		elfzelz	$⊢ L \in (K \dots N) \to L \in ℤ$
34	33	zcnd	$⊢ L \in (K \dots N) \to L \in ℂ$
35	34	adantl	$⊢ (K \in (0 \dots N) \land L \in (K \dots N)) \to L \in ℂ$
36	35	adantl	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|)) \land (K \in (0 \dots N) \land L \in (K \dots N))) \to L \in ℂ$
37	36	addid2d	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|)) \land (K \in (0 \dots N) \land L \in (K \dots N))) \to 0 + L = L$
38	32 37	opeq12d	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|)) \land (K \in (0 \dots N) \land L \in (K \dots N))) \to ⟨0 + K, 0 + L⟩ = ⟨K, L⟩$
39	38	oveq2d	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|)) \land (K \in (0 \dots N) \land L \in (K \dots N))) \to W substr ⟨0 + K, 0 + L⟩ = W substr ⟨K, L⟩$
40	6 27 39	3eqtrd	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|)) \land (K \in (0 \dots N) \land L \in (K \dots N))) \to (W prefix N) substr ⟨K, L⟩ = W substr ⟨K, L⟩$
41	40	ex	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to ((K \in (0 \dots N) \land L \in (K \dots N)) \to (W prefix N) substr ⟨K, L⟩ = W substr ⟨K, L⟩)$

Metamath Proof Explorer

Theorem swrdpfx

Proof