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

Metamath Proof Explorer

Theorem pfxtrcfv0

Description: The first 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 pfxtrcfv0 
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` 0 ) = ( W ` 0 ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> W e. Word V )
2 wrdlenge2n0 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> W =/= (/) )
3 2z 
 |-  2 e. ZZ
4 3 a1i 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 2 e. ZZ )
5 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
6 5 nn0zd 
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
7 6 adantr 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( # ` W ) e. ZZ )
8 simpr 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 2 <_ ( # ` W ) )
9 eluz2 
 |-  ( ( # ` W ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( # ` W ) e. ZZ /\ 2 <_ ( # ` W ) ) )
10 4 7 8 9 syl3anbrc 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` 2 ) )
11 uz2m1nn 
 |-  ( ( # ` W ) e. ( ZZ>= ` 2 ) -> ( ( # ` W ) - 1 ) e. NN )
12 10 11 syl 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. NN )
13 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( ( # ` W ) - 1 ) ) <-> ( ( # ` W ) - 1 ) e. NN )
14 12 13 sylibr 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 0 e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
15 pfxtrcfv 
 |-  ( ( W e. Word V /\ W =/= (/) /\ 0 e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` 0 ) = ( W ` 0 ) )
16 1 2 14 15 syl3anc 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` 0 ) = ( W ` 0 ) )