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

Metamath Proof Explorer

Theorem swrdf

Description: A subword of a word is a function from a half-open range of nonnegative integers of the same length as the subword to the set of symbols for the original word. (Contributed by AV, 13-Nov-2018)

Ref Expression
Assertion swrdf 
|- ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W substr <. M , N >. ) : ( 0 ..^ ( N - M ) ) --> V )

Proof

Step Hyp Ref Expression
1 swrdcl 
 |-  ( W e. Word V -> ( W substr <. M , N >. ) e. Word V )
2 wrdf 
 |-  ( ( W substr <. M , N >. ) e. Word V -> ( W substr <. M , N >. ) : ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) --> V )
3 1 2 syl 
 |-  ( W e. Word V -> ( W substr <. M , N >. ) : ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) --> V )
4 3 3ad2ant1 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W substr <. M , N >. ) : ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) --> V )
5 swrdlen 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. M , N >. ) ) = ( N - M ) )
6 5 oveq2d 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) = ( 0 ..^ ( N - M ) ) )
7 6 feq2d 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( W substr <. M , N >. ) : ( 0 ..^ ( # ` ( W substr <. M , N >. ) ) ) --> V <-> ( W substr <. M , N >. ) : ( 0 ..^ ( N - M ) ) --> V ) )
8 4 7 mpbid 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W substr <. M , N >. ) : ( 0 ..^ ( N - M ) ) --> V )