Users' Mathboxes Mathbox for Andrew Salmon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rr3 Structured version   Visualization version   GIF version

Definition df-rr3 37702
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
StepHypRef Expression
1 crr3c 37686 . 2 class RR3
2 cr 9814 . . 3 class
3 c1 9816 . . . 4 class 1
4 c2 10947 . . . 4 class 2
5 c3 10948 . . . 4 class 3
63, 4, 5ctp 4129 . . 3 class {1, 2, 3}
7 cmap 7744 . . 3 class 𝑚
82, 6, 7co 6549 . 2 class (ℝ ↑𝑚 {1, 2, 3})
91, 8wceq 1475 1 wff RR3 = (ℝ ↑𝑚 {1, 2, 3})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator