df-addr

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

		Ref	Expression
	Assertion	df-addr	$⊢ +_{r} = (x \in V, y \in V ⟼ (v \in ℝ ⟼ x (v) + y (v)))$

Step	Hyp	Ref	Expression
0		cplusr	$class +_{r}$
1		vx	$setvar x$
2		cvv	$class V$
3		vy	$setvar y$
4		vv	$setvar v$
5		cr	$class ℝ$
6	1	cv	$setvar x$
7	4	cv	$setvar v$
8	7 6	cfv	$class x (v)$
9		caddc	$class +$
10	3	cv	$setvar y$
11	7 10	cfv	$class y (v)$
12	8 11 9	co	$class (x (v) + y (v))$
13	4 5 12	cmpt	$class (v \in ℝ ⟼ x (v) + y (v))$
14	1 3 2 2 13	cmpo	$class (x \in V, y \in V ⟼ (v \in ℝ ⟼ x (v) + y (v)))$
15	0 14	wceq	$wff +_{r} = (x \in V, y \in V ⟼ (v \in ℝ ⟼ x (v) + y (v)))$

Metamath Proof Explorer