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	$⊢ ((S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \land X \in (0 ..^L - F)) \to (S substr ⟨F, L⟩) (X) = S (X + F)$

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

Metamath Proof Explorer