pfxlen

Description: Length of a prefix. (Contributed by Stefan O'Rear, 24-Aug-2015) (Revised by AV, 2-May-2020)

		Ref	Expression
	Assertion	pfxlen	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to \|S prefix L\| = L$

Step	Hyp	Ref	Expression
1		pfxfn	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to (S prefix L) Fn (0 ..^L)$
2		hashfn	$⊢ (S prefix L) Fn (0 ..^L) \to \|S prefix L\| = \|(0 ..^L)\|$
3	1 2	syl	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to \|S prefix L\| = \|(0 ..^L)\|$
4		elfznn0	$⊢ L \in (0 \dots \|S\|) \to L \in ℕ_{0}$
5	4	adantl	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to L \in ℕ_{0}$
6		hashfzo0	$⊢ L \in ℕ_{0} \to \|(0 ..^L)\| = L$
7	5 6	syl	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to \|(0 ..^L)\| = L$
8	3 7	eqtrd	$⊢ (S \in Word A \land L \in (0 \dots \|S\|)) \to \|S prefix L\| = L$

Metamath Proof Explorer