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 ⊢ W ∈ Word V ∧ L ∈ 1 … W → lastS ⁡ W prefix L = W ⁡ L − 1

Proof

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