# Metamath Proof Explorer

## Theorem swrdfv

Description: A symbol in an extracted subword, indexed using the subword's indices. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Assertion swrdfv ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {F}\in \left(0\dots {L}\right)\wedge {L}\in \left(0\dots \left|{S}\right|\right)\right)\wedge {X}\in \left(0..^{L}-{F}\right)\right)\to \left({S}\mathrm{substr}⟨{F},{L}⟩\right)\left({X}\right)={S}\left({X}+{F}\right)$

### Proof

Step Hyp Ref Expression
1 swrdval2 ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {F}\in \left(0\dots {L}\right)\wedge {L}\in \left(0\dots \left|{S}\right|\right)\right)\to {S}\mathrm{substr}⟨{F},{L}⟩=\left({x}\in \left(0..^{L}-{F}\right)⟼{S}\left({x}+{F}\right)\right)$
2 1 fveq1d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {F}\in \left(0\dots {L}\right)\wedge {L}\in \left(0\dots \left|{S}\right|\right)\right)\to \left({S}\mathrm{substr}⟨{F},{L}⟩\right)\left({X}\right)=\left({x}\in \left(0..^{L}-{F}\right)⟼{S}\left({x}+{F}\right)\right)\left({X}\right)$
3 fvoveq1 ${⊢}{x}={X}\to {S}\left({x}+{F}\right)={S}\left({X}+{F}\right)$
4 eqid ${⊢}\left({x}\in \left(0..^{L}-{F}\right)⟼{S}\left({x}+{F}\right)\right)=\left({x}\in \left(0..^{L}-{F}\right)⟼{S}\left({x}+{F}\right)\right)$
5 fvex ${⊢}{S}\left({X}+{F}\right)\in \mathrm{V}$
6 3 4 5 fvmpt ${⊢}{X}\in \left(0..^{L}-{F}\right)\to \left({x}\in \left(0..^{L}-{F}\right)⟼{S}\left({x}+{F}\right)\right)\left({X}\right)={S}\left({X}+{F}\right)$
7 2 6 sylan9eq ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {F}\in \left(0\dots {L}\right)\wedge {L}\in \left(0\dots \left|{S}\right|\right)\right)\wedge {X}\in \left(0..^{L}-{F}\right)\right)\to \left({S}\mathrm{substr}⟨{F},{L}⟩\right)\left({X}\right)={S}\left({X}+{F}\right)$