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

Metamath Proof Explorer

Theorem swrdlsw

Description: Extract the last single symbol from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018)

Ref Expression
Assertion swrdlsw 
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = <" ( lastS ` W ) "> )

Proof

Step Hyp Ref Expression
1 hashneq0 
 |-  ( W e. Word V -> ( 0 < ( # ` W ) <-> W =/= (/) ) )
2 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
3 nn0z 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. ZZ )
4 elnnz 
 |-  ( ( # ` W ) e. NN <-> ( ( # ` W ) e. ZZ /\ 0 < ( # ` W ) ) )
5 fzo0end 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
6 4 5 sylbir 
 |-  ( ( ( # ` W ) e. ZZ /\ 0 < ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
7 6 ex 
 |-  ( ( # ` W ) e. ZZ -> ( 0 < ( # ` W ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) )
8 2 3 7 3syl 
 |-  ( W e. Word V -> ( 0 < ( # ` W ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) )
9 1 8 sylbird 
 |-  ( W e. Word V -> ( W =/= (/) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) )
10 9 imp 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
11 swrds1 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( ( ( # ` W ) - 1 ) + 1 ) >. ) = <" ( W ` ( ( # ` W ) - 1 ) ) "> )
12 10 11 syldan 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( ( ( # ` W ) - 1 ) + 1 ) >. ) = <" ( W ` ( ( # ` W ) - 1 ) ) "> )
13 nn0cn 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. CC )
14 ax-1cn 
 |-  1 e. CC
15 13 14 jctir 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) e. CC /\ 1 e. CC ) )
16 npcan 
 |-  ( ( ( # ` W ) e. CC /\ 1 e. CC ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
17 16 eqcomd 
 |-  ( ( ( # ` W ) e. CC /\ 1 e. CC ) -> ( # ` W ) = ( ( ( # ` W ) - 1 ) + 1 ) )
18 2 15 17 3syl 
 |-  ( W e. Word V -> ( # ` W ) = ( ( ( # ` W ) - 1 ) + 1 ) )
19 18 adantr 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) = ( ( ( # ` W ) - 1 ) + 1 ) )
20 19 opeq2d 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> <. ( ( # ` W ) - 1 ) , ( # ` W ) >. = <. ( ( # ` W ) - 1 ) , ( ( ( # ` W ) - 1 ) + 1 ) >. )
21 20 oveq2d 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = ( W substr <. ( ( # ` W ) - 1 ) , ( ( ( # ` W ) - 1 ) + 1 ) >. ) )
22 lsw 
 |-  ( W e. Word V -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
23 22 adantr 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
24 23 s1eqd 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> <" ( lastS ` W ) "> = <" ( W ` ( ( # ` W ) - 1 ) ) "> )
25 12 21 24 3eqtr4d 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = <" ( lastS ` W ) "> )