revfv

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

		Ref	Expression
	Assertion	revfv	$⊢ (W \in Word A \land X \in (0 ..^\|W\|)) \to reverse (W) (X) = W (\|W\| - 1 - X)$

Step	Hyp	Ref	Expression
1		revval	$⊢ W \in Word A \to reverse (W) = (x \in (0 ..^\|W\|) ⟼ W (\|W\| - 1 - x))$
2	1	fveq1d	$⊢ W \in Word A \to reverse (W) (X) = (x \in (0 ..^\|W\|) ⟼ W (\|W\| - 1 - x)) (X)$
3		oveq2	$⊢ x = X \to \|W\| - 1 - x = \|W\| - 1 - X$
4	3	fveq2d	$⊢ x = X \to W (\|W\| - 1 - x) = W (\|W\| - 1 - X)$
5		eqid	$⊢ (x \in (0 ..^\|W\|) ⟼ W (\|W\| - 1 - x)) = (x \in (0 ..^\|W\|) ⟼ W (\|W\| - 1 - x))$
6		fvex	$⊢ W (\|W\| - 1 - X) \in V$
7	4 5 6	fvmpt	$⊢ X \in (0 ..^\|W\|) \to (x \in (0 ..^\|W\|) ⟼ W (\|W\| - 1 - x)) (X) = W (\|W\| - 1 - X)$
8	2 7	sylan9eq	$⊢ (W \in Word A \land X \in (0 ..^\|W\|)) \to reverse (W) (X) = W (\|W\| - 1 - X)$

Metamath Proof Explorer