This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑊 ∈ 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 ) )