# 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 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{W}\right|\right)\right)\to \left({W}\mathrm{substr}⟨{M},{N}⟩\right):\left(0..^{N}-{M}\right)⟶{V}$

### Proof

Step Hyp Ref Expression
1 swrdcl ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{substr}⟨{M},{N}⟩\in \mathrm{Word}{V}$
2 wrdf ${⊢}{W}\mathrm{substr}⟨{M},{N}⟩\in \mathrm{Word}{V}\to \left({W}\mathrm{substr}⟨{M},{N}⟩\right):\left(0..^\left|{W}\mathrm{substr}⟨{M},{N}⟩\right|\right)⟶{V}$
3 1 2 syl ${⊢}{W}\in \mathrm{Word}{V}\to \left({W}\mathrm{substr}⟨{M},{N}⟩\right):\left(0..^\left|{W}\mathrm{substr}⟨{M},{N}⟩\right|\right)⟶{V}$
4 3 3ad2ant1 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{W}\right|\right)\right)\to \left({W}\mathrm{substr}⟨{M},{N}⟩\right):\left(0..^\left|{W}\mathrm{substr}⟨{M},{N}⟩\right|\right)⟶{V}$
5 swrdlen ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{W}\right|\right)\right)\to \left|{W}\mathrm{substr}⟨{M},{N}⟩\right|={N}-{M}$
6 5 oveq2d ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{W}\right|\right)\right)\to \left(0..^\left|{W}\mathrm{substr}⟨{M},{N}⟩\right|\right)=\left(0..^{N}-{M}\right)$
7 6 feq2d ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{W}\right|\right)\right)\to \left(\left({W}\mathrm{substr}⟨{M},{N}⟩\right):\left(0..^\left|{W}\mathrm{substr}⟨{M},{N}⟩\right|\right)⟶{V}↔\left({W}\mathrm{substr}⟨{M},{N}⟩\right):\left(0..^{N}-{M}\right)⟶{V}\right)$
8 4 7 mpbid ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{W}\right|\right)\right)\to \left({W}\mathrm{substr}⟨{M},{N}⟩\right):\left(0..^{N}-{M}\right)⟶{V}$