Metamath Proof Explorer

Theorem lsw0

Description: The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 19-Mar-2018) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion lsw0 
|- ( ( W e. Word V /\ ( # ` W ) = 0 ) -> ( lastS ` W ) = (/) )

Proof

Step Hyp Ref Expression
1 lsw 
 |-  ( W e. Word V -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
2 1 adantr 
 |-  ( ( W e. Word V /\ ( # ` W ) = 0 ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
3 fvoveq1 
 |-  ( ( # ` W ) = 0 -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` ( 0 - 1 ) ) )
4 wrddm 
 |-  ( W e. Word V -> dom W = ( 0 ..^ ( # ` W ) ) )
5 1nn 
 |-  1 e. NN
6 nnnle0 
 |-  ( 1 e. NN -> -. 1 <_ 0 )
7 5 6 ax-mp 
 |-  -. 1 <_ 0
8 0re 
 |-  0 e. RR
9 1re 
 |-  1 e. RR
10 8 9 subge0i 
 |-  ( 0 <_ ( 0 - 1 ) <-> 1 <_ 0 )
11 7 10 mtbir 
 |-  -. 0 <_ ( 0 - 1 )
12 elfzole1 
 |-  ( ( 0 - 1 ) e. ( 0 ..^ ( # ` W ) ) -> 0 <_ ( 0 - 1 ) )
13 11 12 mto 
 |-  -. ( 0 - 1 ) e. ( 0 ..^ ( # ` W ) )
14 eleq2 
 |-  ( dom W = ( 0 ..^ ( # ` W ) ) -> ( ( 0 - 1 ) e. dom W <-> ( 0 - 1 ) e. ( 0 ..^ ( # ` W ) ) ) )
15 13 14 mtbiri 
 |-  ( dom W = ( 0 ..^ ( # ` W ) ) -> -. ( 0 - 1 ) e. dom W )
16 ndmfv 
 |-  ( -. ( 0 - 1 ) e. dom W -> ( W ` ( 0 - 1 ) ) = (/) )
17 4 15 16 3syl 
 |-  ( W e. Word V -> ( W ` ( 0 - 1 ) ) = (/) )
18 3 17 sylan9eqr 
 |-  ( ( W e. Word V /\ ( # ` W ) = 0 ) -> ( W ` ( ( # ` W ) - 1 ) ) = (/) )
19 2 18 eqtrd 
 |-  ( ( W e. Word V /\ ( # ` W ) = 0 ) -> ( lastS ` W ) = (/) )