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	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : ( 0 ..^ ( 𝑁 − 𝑀 ) ) ⟶ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		swrdcl	⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word 𝑉 )
2		wrdf	⊢ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word 𝑉 → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ⟶ 𝑉 )
3	1 2	syl	⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ⟶ 𝑉 )
4	3	3ad2ant1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ⟶ 𝑉 )
5		swrdlen	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( 𝑁 − 𝑀 ) )
6	5	oveq2d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) = ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
7	6	feq2d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) ⟶ 𝑉 ↔ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : ( 0 ..^ ( 𝑁 − 𝑀 ) ) ⟶ 𝑉 ) )
8	4 7	mpbid	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : ( 0 ..^ ( 𝑁 − 𝑀 ) ) ⟶ 𝑉 )