Database
REAL AND COMPLEX NUMBERS
Words over a set
Subwords/substrings
swrdvalfn
Metamath Proof Explorer
Description: Value of the subword extractor as function with domain. (Contributed by Alexander van der Vekens , 28-Mar-2018) (Proof shortened by AV , 2-May-2020)
Ref
Expression
Assertion
swrdvalfn
⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr 〈 𝐹 , 𝐿 〉 ) Fn ( 0 ..^ ( 𝐿 − 𝐹 ) ) )
Proof
Step
Hyp
Ref
Expression
1
swrdf
⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr 〈 𝐹 , 𝐿 〉 ) : ( 0 ..^ ( 𝐿 − 𝐹 ) ) ⟶ 𝑉 )
2
1
ffnd
⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr 〈 𝐹 , 𝐿 〉 ) Fn ( 0 ..^ ( 𝐿 − 𝐹 ) ) )