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

Definition df-rr3 27785
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 27769 . 2  class  RR 3
2 cr 8752 . . 3  class  RR
3 c1 8754 . . . 4  class  1
4 c2 9811 . . . 4  class  2
5 c3 9812 . . . 4  class  3
63, 4, 5ctp 3655 . . 3  class  { 1 ,  2 ,  3 }
7 cmap 6788 . . 3  class  ^m
82, 6, 7co 5874 . 2  class  ( RR 
^m  { 1 ,  2 ,  3 } )
91, 8wceq 1632 1  wff  RR 3  =  ( RR  ^m  { 1 ,  2 ,  3 } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator