Definition df-rr3 44496

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 = (ℝ ↑m {1, 2, 3})

Detailed syntax breakdown of Definition df-rr3

Step	Hyp	Ref	Expression
1		crr3c 44480	. 2 class RR3
2		cr 11154	. . 3 class ℝ
3		c1 11156	. . . 4 class 1
4		c2 12321	. . . 4 class 2
5		c3 12322	. . . 4 class 3
6	3, 4, 5	ctp 4630	. . 3 class {1, 2, 3}
7		cmap 8866	. . 3 class ↑m
8	2, 6, 7	co 7431	. 2 class (ℝ ↑m {1, 2, 3})
9	1, 8	wceq 1540	1 wff RR3 = (ℝ ↑m {1, 2, 3})

This definition is referenced by: (None)