pfxres

Description: Value of the prefix extractor as the restriction of a word. (Contributed by Stefan O'Rear, 24-Aug-2015) (Revised by AV, 2-May-2020)

		Ref	Expression
	Assertion	pfxres	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to S prefix L = {S ↾}_{(0 ..^L)}$

Step	Hyp	Ref	Expression
1		pfxmpt	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to S prefix L = (x \in (0 ..^L) ⟼ S (x))$
2		wrdf	$⊢ S \in Word A \to S : (0 ..^\|S\|) ⟶ A$
3	2	adantr	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to S : (0 ..^\|S\|) ⟶ A$
4		elfzuz3	$⊢ L \in (0 \dots \|S\|) \to \|S\| \in ℤ_{\geq L}$
5	4	adantl	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to \|S\| \in ℤ_{\geq L}$
6		fzoss2	$⊢ \|S\| \in ℤ_{\geq L} \to (0 ..^L) \subseteq (0 ..^\|S\|)$
7	5 6	syl	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to (0 ..^L) \subseteq (0 ..^\|S\|)$
8	3 7	feqresmpt	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to {S ↾}_{(0 ..^L)} = (x \in (0 ..^L) ⟼ S (x))$
9	1 8	eqtr4d	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to S prefix L = {S ↾}_{(0 ..^L)}$

Metamath Proof Explorer