Metamath Proof Explorer

Theorem pfxtrcfv

Description: A symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018) (Revised by AV, 3-May-2020)

Ref Expression
Assertion pfxtrcfv 
|- ( ( W e. Word V /\ W =/= (/) /\ I e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` I ) = ( W ` I ) )

Proof

Step Hyp Ref Expression
1 wrdfin 
 |-  ( W e. Word V -> W e. Fin )
2 1elfz0hash 
 |-  ( ( W e. Fin /\ W =/= (/) ) -> 1 e. ( 0 ... ( # ` W ) ) )
3 1 2 sylan 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> 1 e. ( 0 ... ( # ` W ) ) )
4 lennncl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. NN )
5 elfz1end 
 |-  ( ( # ` W ) e. NN <-> ( # ` W ) e. ( 1 ... ( # ` W ) ) )
6 4 5 sylib 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. ( 1 ... ( # ` W ) ) )
7 3 6 jca 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( 1 e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 1 ... ( # ` W ) ) ) )
8 7 3adant3 
 |-  ( ( W e. Word V /\ W =/= (/) /\ I e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( 1 e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 1 ... ( # ` W ) ) ) )
9 fz0fzdiffz0 
 |-  ( ( 1 e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 1 ... ( # ` W ) ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) )
10 8 9 syl 
 |-  ( ( W e. Word V /\ W =/= (/) /\ I e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) )
11 pfxfv 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` I ) = ( W ` I ) )
12 10 11 syld3an2 
 |-  ( ( W e. Word V /\ W =/= (/) /\ I e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` I ) = ( W ` I ) )