addrval

Description: Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012)

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

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in C \to A \in V$
2		elex	$⊢ B \in D \to B \in V$
3		fveq1	$⊢ x = A \to x (v) = A (v)$
4		fveq1	$⊢ y = B \to y (v) = B (v)$
5	3 4	oveqan12d	$⊢ (x = A \land y = B) \to x (v) + y (v) = A (v) + B (v)$
6	5	mpteq2dv	$⊢ (x = A \land y = B) \to (v \in ℝ ⟼ x (v) + y (v)) = (v \in ℝ ⟼ A (v) + B (v))$
7		df-addr	$⊢ +_{r} = (x \in V, y \in V ⟼ (v \in ℝ ⟼ x (v) + y (v)))$
8		reex	$⊢ ℝ \in V$
9	8	mptex	$⊢ (v \in ℝ ⟼ A (v) + B (v)) \in V$
10	6 7 9	ovmpoa	$⊢ (A \in V \land B \in V) \to A +_{r} B = (v \in ℝ ⟼ A (v) + B (v))$
11	1 2 10	syl2an	$⊢ (A \in C \land B \in D) \to A +_{r} B = (v \in ℝ ⟼ A (v) + B (v))$

Metamath Proof Explorer