pfxmpt

Description: Value of the prefix extractor as a mapping. (Contributed by AV, 2-May-2020)

		Ref	Expression
	Assertion	pfxmpt	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to S prefix L = (x \in (0 ..^L) ⟼ S (x))$

Proof

Step	Hyp	Ref	Expression
1		elfznn0	$⊢ L \in (0 \dots \|S\|) \to L \in ℕ_{0}$
2		pfxval	$⊢ (S \in Word A \land L \in ℕ_{0}) \to S prefix L = S substr ⟨0, L⟩$
3	1 2	sylan2	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to S prefix L = S substr ⟨0, L⟩$
4		simpl	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to S \in Word A$
5	1	adantl	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to L \in ℕ_{0}$
6		0elfz	$⊢ L \in ℕ_{0} \to 0 \in (0 \dots L)$
7	5 6	syl	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to 0 \in (0 \dots L)$
8		simpr	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to L \in (0 \dots \|S\|)$
9		swrdval2	$⊢ (S \in Word A \land 0 \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to S substr ⟨0, L⟩ = (x \in (0 ..^L - 0) ⟼ S (x + 0))$
10	4 7 8 9	syl3anc	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to S substr ⟨0, L⟩ = (x \in (0 ..^L - 0) ⟼ S (x + 0))$
11		nn0cn	$⊢ L \in ℕ_{0} \to L \in ℂ$
12	11	subid1d	$⊢ L \in ℕ_{0} \to L - 0 = L$
13	1 12	syl	$⊢ L \in (0 \dots \|S\|) \to L - 0 = L$
14	13	oveq2d	$⊢ L \in (0 \dots \|S\|) \to (0 ..^L - 0) = (0 ..^L)$
15	14	adantl	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to (0 ..^L - 0) = (0 ..^L)$
16		elfzonn0	$⊢ x \in (0 ..^L - 0) \to x \in ℕ_{0}$
17		nn0cn	$⊢ x \in ℕ_{0} \to x \in ℂ$
18	17	addid1d	$⊢ x \in ℕ_{0} \to x + 0 = x$
19	16 18	syl	$⊢ x \in (0 ..^L - 0) \to x + 0 = x$
20	19	fveq2d	$⊢ x \in (0 ..^L - 0) \to S (x + 0) = S (x)$
21	20	adantl	$⊢ ((S \in Word A \land L \in (0 \dots \|S\|)) \land x \in (0 ..^L - 0)) \to S (x + 0) = S (x)$
22	15 21	mpteq12dva	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to (x \in (0 ..^L - 0) ⟼ S (x + 0)) = (x \in (0 ..^L) ⟼ S (x))$
23	3 10 22	3eqtrd	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to S prefix L = (x \in (0 ..^L) ⟼ S (x))$

Metamath Proof Explorer

Theorem pfxmpt

Proof