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 
|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix L ) ` 0 ) = ( W ` 0 ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> W e. Word V )
2 fz1ssfz0 
 |-  ( 1 ... ( # ` W ) ) C_ ( 0 ... ( # ` W ) )
3 2 sseli 
 |-  ( L e. ( 1 ... ( # ` W ) ) -> L e. ( 0 ... ( # ` W ) ) )
4 3 adantl 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> L e. ( 0 ... ( # ` W ) ) )
5 elfznn 
 |-  ( L e. ( 1 ... ( # ` W ) ) -> L e. NN )
6 5 adantl 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> L e. NN )
7 lbfzo0 
 |-  ( 0 e. ( 0 ..^ L ) <-> L e. NN )
8 6 7 sylibr 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> 0 e. ( 0 ..^ L ) )
9 pfxfv 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ 0 e. ( 0 ..^ L ) ) -> ( ( W prefix L ) ` 0 ) = ( W ` 0 ) )
10 1 4 8 9 syl3anc 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix L ) ` 0 ) = ( W ` 0 ) )