Metamath Proof Explorer

Theorem addrfv

Description: Vector addition at a value. The operation takes each vector A and B and forms a new vector whose values are the sum of each of the values of A and B . (Contributed by Andrew Salmon, 27-Jan-2012)

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

Proof

Step	Hyp	Ref	Expression
1		addrval	$⊢ (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)$