# 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 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {L}\in \left(1\dots \left|{W}\right|\right)\right)\to \left({W}\mathrm{prefix}{L}\right)\left(0\right)={W}\left(0\right)$

### Proof

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