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

Metamath Proof Explorer

Theorem revfv

Description: Reverse of a word at a point. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Assertion revfv ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ 𝑋 ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 revval ⊢ ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ 𝑊 ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) )
2 1 fveq1d ⊢ ( 𝑊 ∈ Word 𝐴 → ( ( reverse ‘ 𝑊 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) ‘ 𝑋 ) )
3 oveq2 ⊢ ( 𝑥 = 𝑋 → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑋 ) )
4 3 fveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑋 ) ) )
5 eqid ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) )
6 fvex ⊢ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑋 ) ) ∈ V
7 4 5 6 fvmpt ⊢ ( 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) ‘ 𝑋 ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑋 ) ) )
8 2 7 sylan9eq ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ 𝑋 ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑋 ) ) )