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

Definition df-rr3 27682
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 27666 . 2  class  RR 3
2 cr 8736 . . 3  class  RR
3 c1 8738 . . . 4  class  1
4 c2 9795 . . . 4  class  2
5 c3 9796 . . . 4  class  3
63, 4, 5ctp 3642 . . 3  class  { 1 ,  2 ,  3 }
7 cmap 6772 . . 3  class  ^m
82, 6, 7co 5858 . 2  class  ( RR 
^m  { 1 ,  2 ,  3 } )
91, 8wceq 1623 1  wff  RR 3  =  ( RR  ^m  { 1 ,  2 ,  3 } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator