Metamath Proof Explorer

Theorem pfxtrcfvl

Description: The last symbol in a word truncated by one symbol. (Contributed by AV, 16-Jun-2018) (Revised by AV, 5-May-2020)

Ref Expression
Assertion pfxtrcfvl 
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( W ` ( ( # ` W ) - 2 ) ) )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 1 a1i 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 2 e. ZZ )
3 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
4 3 nn0zd 
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
5 4 adantr 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( # ` W ) e. ZZ )
6 simpr 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 2 <_ ( # ` W ) )
7 eluz2 
 |-  ( ( # ` W ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( # ` W ) e. ZZ /\ 2 <_ ( # ` W ) ) )
8 2 5 6 7 syl3anbrc 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` 2 ) )
9 ige2m1fz1 
 |-  ( ( # ` W ) e. ( ZZ>= ` 2 ) -> ( ( # ` W ) - 1 ) e. ( 1 ... ( # ` W ) ) )
10 8 9 syl 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( 1 ... ( # ` W ) ) )
11 pfxfvlsw 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( W ` ( ( ( # ` W ) - 1 ) - 1 ) ) )
12 10 11 syldan 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( W ` ( ( ( # ` W ) - 1 ) - 1 ) ) )
13 3 nn0cnd 
 |-  ( W e. Word V -> ( # ` W ) e. CC )
14 sub1m1 
 |-  ( ( # ` W ) e. CC -> ( ( ( # ` W ) - 1 ) - 1 ) = ( ( # ` W ) - 2 ) )
15 13 14 syl 
 |-  ( W e. Word V -> ( ( ( # ` W ) - 1 ) - 1 ) = ( ( # ` W ) - 2 ) )
16 15 adantr 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) - 1 ) = ( ( # ` W ) - 2 ) )
17 16 fveq2d 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( W ` ( ( ( # ` W ) - 1 ) - 1 ) ) = ( W ` ( ( # ` W ) - 2 ) ) )
18 12 17 eqtrd 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( W ` ( ( # ` W ) - 2 ) ) )