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

Metamath Proof Explorer

Theorem pfxfvlsw

Description: The last symbol in a nonempty prefix of a word. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 3-May-2020)

Ref Expression
Assertion pfxfvlsw ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 prefix 𝐿 ) ) = ( 𝑊 ‘ ( 𝐿 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 pfxcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) ∈ Word 𝑉 )
2 1 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) ∈ Word 𝑉 )
3 lsw ⊢ ( ( 𝑊 prefix 𝐿 ) ∈ Word 𝑉 → ( lastS ‘ ( 𝑊 prefix 𝐿 ) ) = ( ( 𝑊 prefix 𝐿 ) ‘ ( ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) − 1 ) ) )
4 2 3 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 prefix 𝐿 ) ) = ( ( 𝑊 prefix 𝐿 ) ‘ ( ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) − 1 ) ) )
5 fz1ssfz0 ⊢ ( 1 ... ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑊 ) )
6 5 sseli ⊢ ( 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
7 pfxlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) = 𝐿 )
8 6 7 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) = 𝐿 )
9 8 fvoveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐿 ) ‘ ( ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) − 1 ) ) = ( ( 𝑊 prefix 𝐿 ) ‘ ( 𝐿 − 1 ) ) )
10 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 )
11 6 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
12 elfznn ⊢ ( 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℕ )
13 fzo0end ⊢ ( 𝐿 ∈ ℕ → ( 𝐿 − 1 ) ∈ ( 0 ..^ 𝐿 ) )
14 12 13 syl ⊢ ( 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( 𝐿 − 1 ) ∈ ( 0 ..^ 𝐿 ) )
15 14 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝐿 − 1 ) ∈ ( 0 ..^ 𝐿 ) )
16 pfxfv ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝐿 − 1 ) ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑊 prefix 𝐿 ) ‘ ( 𝐿 − 1 ) ) = ( 𝑊 ‘ ( 𝐿 − 1 ) ) )
17 10 11 15 16 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐿 ) ‘ ( 𝐿 − 1 ) ) = ( 𝑊 ‘ ( 𝐿 − 1 ) ) )
18 4 9 17 3eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 prefix 𝐿 ) ) = ( 𝑊 ‘ ( 𝐿 − 1 ) ) )