Metamath Proof Explorer

Theorem pfxfv0

Description: The first symbol of a prefix is the first symbol of the word. (Contributed by Alexander van der Vekens, 16-Jun-2018) (Revised by AV, 3-May-2020)

		Ref	Expression
	Assertion	pfxfv0	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to (W prefix L) (0) = W (0)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to W \in Word V$
2		fz1ssfz0	$⊢ (1 \dots \|W\|) \subseteq (0 \dots \|W\|)$
3	2	sseli	$⊢ L \in (1 \dots \|W\|) \to L \in (0 \dots \|W\|)$
4	3	adantl	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to L \in (0 \dots \|W\|)$
5		elfznn	$⊢ L \in (1 \dots \|W\|) \to L \in ℕ$
6	5	adantl	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to L \in ℕ$
7		lbfzo0	$⊢ 0 \in (0 ..^L) \leftrightarrow L \in ℕ$
8	6 7	sylibr	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to 0 \in (0 ..^L)$
9		pfxfv	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land 0 \in (0 ..^L)) \to (W prefix L) (0) = W (0)$
10	1 4 8 9	syl3anc	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to (W prefix L) (0) = W (0)$