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	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐿 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 )
2		fz1ssfz0	⊢ ( 1 ... ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑊 ) )
3	2	sseli	⊢ ( 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
4	3	adantl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
5		elfznn	⊢ ( 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℕ )
6	5	adantl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → 𝐿 ∈ ℕ )
7		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ 𝐿 ) ↔ 𝐿 ∈ ℕ )
8	6 7	sylibr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → 0 ∈ ( 0 ..^ 𝐿 ) )
9		pfxfv	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 0 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑊 prefix 𝐿 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
10	1 4 8 9	syl3anc	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐿 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )