This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑋 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ‘ 𝑋 ) = ( 𝑆 ‘ ( 𝑋 + 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 swrdval2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) )
2 1 fveq1d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ‘ 𝑋 ) = ( ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) ‘ 𝑋 ) )
3 fvoveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) = ( 𝑆 ‘ ( 𝑋 + 𝐹 ) ) )
4 eqid ⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) )
5 fvex ⊢ ( 𝑆 ‘ ( 𝑋 + 𝐹 ) ) ∈ V
6 3 4 5 fvmpt ⊢ ( 𝑋 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) → ( ( 𝑥 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝐹 ) ) ) ‘ 𝑋 ) = ( 𝑆 ‘ ( 𝑋 + 𝐹 ) ) )
7 2 6 sylan9eq ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑋 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ‘ 𝑋 ) = ( 𝑆 ‘ ( 𝑋 + 𝐹 ) ) )