Definition df-addr

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

	Ref	Expression
Assertion	df-addr	|- +r = ( x e. _V , y e. _V |-> ( v e. RR |-> ( ( x ` v ) + ( y ` v ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplusr	|- +r
1		vx	|- x
2		cvv	|- _V
3		vy	|- y
4		vv	|- v
5		cr	|- RR
6	1	cv	|- x
7	4	cv	|- v
8	7 6	cfv	|- ( x ` v )
9		caddc	|- +
10	3	cv	|- y
11	7 10	cfv	|- ( y ` v )
12	8 11 9	co	|- ( ( x ` v ) + ( y ` v ) )
13	4 5 12	cmpt	|- ( v e. RR |-> ( ( x ` v ) + ( y ` v ) ) )
14	1 3 2 2 13	cmpo	|- ( x e. _V , y e. _V |-> ( v e. RR |-> ( ( x ` v ) + ( y ` v ) ) ) )
15	0 14	wceq	|- +r = ( x e. _V , y e. _V |-> ( v e. RR |-> ( ( x ` v ) + ( y ` v ) ) ) )