subrfv

Description: Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012)

		Ref	Expression
	Assertion	subrfv	$⊢ (A \in E \land B \in D \land C \in ℝ) \to (A -_{r} B) (C) = A (C) - B (C)$

Step	Hyp	Ref	Expression
1		subrval	$⊢ (A \in E \land B \in D) \to A -_{r} B = (x \in ℝ ⟼ A (x) - B (x))$
2	1	fveq1d	$⊢ (A \in E \land B \in D) \to (A -_{r} B) (C) = (x \in ℝ ⟼ A (x) - B (x)) (C)$
3		fveq2	$⊢ x = C \to A (x) = A (C)$
4		fveq2	$⊢ x = C \to B (x) = B (C)$
5	3 4	oveq12d	$⊢ x = C \to A (x) - B (x) = A (C) - B (C)$
6		eqid	$⊢ (x \in ℝ ⟼ A (x) - B (x)) = (x \in ℝ ⟼ A (x) - B (x))$
7		ovex	$⊢ A (C) - B (C) \in V$
8	5 6 7	fvmpt	$⊢ C \in ℝ \to (x \in ℝ ⟼ A (x) - B (x)) (C) = A (C) - B (C)$
9	2 8	sylan9eq	$⊢ ((A \in E \land B \in D) \land C \in ℝ) \to (A -_{r} B) (C) = A (C) - B (C)$
10	9	3impa	$⊢ (A \in E \land B \in D \land C \in ℝ) \to (A -_{r} B) (C) = A (C) - B (C)$

Metamath Proof Explorer