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 )