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 ⊢ W ∈ Word A ∧ X ∈ 0 ..^ W → reverse ⁡ W ⁡ X = W ⁡ W - 1 - X

Proof

Step Hyp Ref Expression
1 revval ⊢ W ∈ Word A → reverse ⁡ W = x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x
2 1 fveq1d ⊢ W ∈ Word A → reverse ⁡ W ⁡ X = x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x ⁡ X
3 oveq2 ⊢ x = X → W - 1 - x = W - 1 - X
4 3 fveq2d ⊢ x = X → W ⁡ W - 1 - x = W ⁡ W - 1 - X
5 eqid ⊢ x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x = x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x
6 fvex ⊢ W ⁡ W - 1 - X ∈ V
7 4 5 6 fvmpt ⊢ X ∈ 0 ..^ W → x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x ⁡ X = W ⁡ W - 1 - X
8 2 7 sylan9eq ⊢ W ∈ Word A ∧ X ∈ 0 ..^ W → reverse ⁡ W ⁡ X = W ⁡ W - 1 - X