Metamath Proof Explorer

Theorem pfxrn3

Description: Express the range of a prefix of a word. Stronger version of pfxrn2 . (Contributed by Thierry Arnoux, 13-Dec-2023)

		Ref	Expression
	Assertion	pfxrn3	$⊢ (W \in Word S \land L \in (0 \dots \|W\|)) \to ran (W prefix L) = W [(0 ..^L)]$

Step	Hyp	Ref	Expression
1		pfxres	$⊢ (W \in Word S \land L \in (0 \dots \|W\|)) \to W prefix L = {W ↾}_{(0 ..^L)}$
2	1	rneqd	$⊢ (W \in Word S \land L \in (0 \dots \|W\|)) \to ran (W prefix L) = ran ({W ↾}_{(0 ..^L)})$
3		df-ima	$⊢ W [(0 ..^L)] = ran ({W ↾}_{(0 ..^L)})$
4	2 3	eqtr4di	$⊢ (W \in Word S \land L \in (0 \dots \|W\|)) \to ran (W prefix L) = W [(0 ..^L)]$