Definition df-rr3 38681

Description: Define the set of all points RR3. We define each point A as a function to allow the use of vector addition and subtraction as well as scalar multiplication in our proofs. (Contributed by Andrew Salmon, 15-Jul-2012.)

Assertion

Ref	Expression
df-rr3	|- RR3 = ( RR ^m { 1 , 2 , 3 } )

Detailed syntax breakdown of Definition df-rr3

Step	Hyp	Ref	Expression
1		crr3c 38665	. 2 class RR3
2		cr 9935	. . 3 class RR
3		c1 9937	. . . 4 class 1
4		c2 11070	. . . 4 class 2
5		c3 11071	. . . 4 class 3
6	3, 4, 5	ctp 4181	. . 3 class { 1 , 2 , 3 }
7		cmap 7857	. . 3 class ^m
8	2, 6, 7	co 6650	. 2 class ( RR ^m { 1 , 2 , 3 } )
9	1, 8	wceq 1483	1 wff RR3 = ( RR ^m { 1 , 2 , 3 } )

This definition is referenced by: (None)