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

Metamath Proof Explorer

Theorem pfxfvlsw

Description: The last symbol in a nonempty prefix of a word. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 3-May-2020)

Ref Expression
Assertion pfxfvlsw 
|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix L ) ) = ( W ` ( L - 1 ) ) )

Proof

Step Hyp Ref Expression
1 pfxcl 
 |-  ( W e. Word V -> ( W prefix L ) e. Word V )
2 1 adantr 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( W prefix L ) e. Word V )
3 lsw 
 |-  ( ( W prefix L ) e. Word V -> ( lastS ` ( W prefix L ) ) = ( ( W prefix L ) ` ( ( # ` ( W prefix L ) ) - 1 ) ) )
4 2 3 syl 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix L ) ) = ( ( W prefix L ) ` ( ( # ` ( W prefix L ) ) - 1 ) ) )
5 fz1ssfz0 
 |-  ( 1 ... ( # ` W ) ) C_ ( 0 ... ( # ` W ) )
6 5 sseli 
 |-  ( L e. ( 1 ... ( # ` W ) ) -> L e. ( 0 ... ( # ` W ) ) )
7 pfxlen 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix L ) ) = L )
8 6 7 sylan2 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( # ` ( W prefix L ) ) = L )
9 8 fvoveq1d 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix L ) ` ( ( # ` ( W prefix L ) ) - 1 ) ) = ( ( W prefix L ) ` ( L - 1 ) ) )
10 simpl 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> W e. Word V )
11 6 adantl 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> L e. ( 0 ... ( # ` W ) ) )
12 elfznn 
 |-  ( L e. ( 1 ... ( # ` W ) ) -> L e. NN )
13 fzo0end 
 |-  ( L e. NN -> ( L - 1 ) e. ( 0 ..^ L ) )
14 12 13 syl 
 |-  ( L e. ( 1 ... ( # ` W ) ) -> ( L - 1 ) e. ( 0 ..^ L ) )
15 14 adantl 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( L - 1 ) e. ( 0 ..^ L ) )
16 pfxfv 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ ( L - 1 ) e. ( 0 ..^ L ) ) -> ( ( W prefix L ) ` ( L - 1 ) ) = ( W ` ( L - 1 ) ) )
17 10 11 15 16 syl3anc 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix L ) ` ( L - 1 ) ) = ( W ` ( L - 1 ) ) )
18 4 9 17 3eqtrd 
 |-  ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix L ) ) = ( W ` ( L - 1 ) ) )