Definition df-rr3 38681

Description: Define the set of all points RR3. We define each point 𝐴 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 = (ℝ ↑𝑚 {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 ℝ
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 ↑𝑚
8	2, 6, 7	co 6650	. 2 class (ℝ ↑𝑚 {1, 2, 3})
9	1, 8	wceq 1483	1 wff RR3 = (ℝ ↑𝑚 {1, 2, 3})

This definition is referenced by: (None)