Metamath Proof Explorer

Theorem swrdrlen

Description: Length of a right-anchored subword. (Contributed by Alexander van der Vekens, 5-Apr-2018)

Ref Expression
Assertion swrdrlen 
|- ( ( W e. Word V /\ I e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. I , ( # ` W ) >. ) ) = ( ( # ` W ) - I ) )

Proof

Step Hyp Ref Expression
1 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
2 nn0fz0 
 |-  ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
3 1 2 sylib 
 |-  ( W e. Word V -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
4 3 adantr 
 |-  ( ( W e. Word V /\ I e. ( 0 ... ( # ` W ) ) ) -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
5 swrdlen 
 |-  ( ( W e. Word V /\ I e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. I , ( # ` W ) >. ) ) = ( ( # ` W ) - I ) )
6 4 5 mpd3an3 
 |-  ( ( W e. Word V /\ I e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. I , ( # ` W ) >. ) ) = ( ( # ` W ) - I ) )