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 ( ( 𝑊 ∈ 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 ..^ ( 𝑁 − 𝑀 ) ) ⟶ 𝑉 )