pfxfv

Description: A symbol in a prefix of a word, indexed using the prefix' indices. (Contributed by Alexander van der Vekens, 16-Jun-2018) (Revised by AV, 3-May-2020)

		Ref	Expression
	Assertion	pfxfv	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land I \in (0 ..^L)) \to (W prefix L) (I) = W (I)$

Proof

Step	Hyp	Ref	Expression
1		elfznn0	$⊢ L \in (0 \dots \|W\|) \to L \in ℕ_{0}$
2		pfxval	$⊢ (W \in Word V \land L \in ℕ_{0}) \to W prefix L = W substr ⟨0, L⟩$
3	1 2	sylan2	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to W prefix L = W substr ⟨0, L⟩$
4	3	3adant3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land I \in (0 ..^L)) \to W prefix L = W substr ⟨0, L⟩$
5	4	fveq1d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land I \in (0 ..^L)) \to (W prefix L) (I) = (W substr ⟨0, L⟩) (I)$
6		simp1	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land I \in (0 ..^L)) \to W \in Word V$
7		0elfz	$⊢ L \in ℕ_{0} \to 0 \in (0 \dots L)$
8	1 7	syl	$⊢ L \in (0 \dots \|W\|) \to 0 \in (0 \dots L)$
9	8	3ad2ant2	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land I \in (0 ..^L)) \to 0 \in (0 \dots L)$
10		simp2	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land I \in (0 ..^L)) \to L \in (0 \dots \|W\|)$
11	1	nn0cnd	$⊢ L \in (0 \dots \|W\|) \to L \in ℂ$
12	11	subid1d	$⊢ L \in (0 \dots \|W\|) \to L - 0 = L$
13	12	eqcomd	$⊢ L \in (0 \dots \|W\|) \to L = L - 0$
14	13	oveq2d	$⊢ L \in (0 \dots \|W\|) \to (0 ..^L) = (0 ..^L - 0)$
15	14	eleq2d	$⊢ L \in (0 \dots \|W\|) \to (I \in (0 ..^L) \leftrightarrow I \in (0 ..^L - 0))$
16	15	biimpd	$⊢ L \in (0 \dots \|W\|) \to (I \in (0 ..^L) \to I \in (0 ..^L - 0))$
17	16	a1i	$⊢ W \in Word V \to (L \in (0 \dots \|W\|) \to (I \in (0 ..^L) \to I \in (0 ..^L - 0)))$
18	17	3imp	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land I \in (0 ..^L)) \to I \in (0 ..^L - 0)$
19		swrdfv	$⊢ ((W \in Word V \land 0 \in (0 \dots L) \land L \in (0 \dots \|W\|)) \land I \in (0 ..^L - 0)) \to (W substr ⟨0, L⟩) (I) = W (I + 0)$
20	6 9 10 18 19	syl31anc	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land I \in (0 ..^L)) \to (W substr ⟨0, L⟩) (I) = W (I + 0)$
21		elfzoelz	$⊢ I \in (0 ..^L) \to I \in ℤ$
22	21	zcnd	$⊢ I \in (0 ..^L) \to I \in ℂ$
23	22	addridd	$⊢ I \in (0 ..^L) \to I + 0 = I$
24	23	3ad2ant3	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land I \in (0 ..^L)) \to I + 0 = I$
25	24	fveq2d	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land I \in (0 ..^L)) \to W (I + 0) = W (I)$
26	5 20 25	3eqtrd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land I \in (0 ..^L)) \to (W prefix L) (I) = W (I)$

Metamath Proof Explorer

Theorem pfxfv

Proof