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

Definition df-rr3 27649
Description: Define the set of all points  RR 3. 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  |-  RR 3  =  ( RR  ^m  { 1 ,  2 ,  3 } )

Detailed syntax breakdown of Definition df-rr3
StepHypRef Expression
1 crr3c 27633 . 2  class  RR 3
2 cr 8981 . . 3  class  RR
3 c1 8983 . . . 4  class  1
4 c2 10041 . . . 4  class  2
5 c3 10042 . . . 4  class  3
63, 4, 5ctp 3808 . . 3  class  { 1 ,  2 ,  3 }
7 cmap 7010 . . 3  class  ^m
82, 6, 7co 6073 . 2  class  ( RR 
^m  { 1 ,  2 ,  3 } )
91, 8wceq 1652 1  wff  RR 3  =  ( RR  ^m  { 1 ,  2 ,  3 } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator