Description: Define the set of all points RR3 . 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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-rr3 | |- RR3 = ( RR ^m { 1 , 2 , 3 } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | crr3c | |- RR3 |
|
| 1 | cr | |- RR |
|
| 2 | cmap | |- ^m |
|
| 3 | c1 | |- 1 |
|
| 4 | c2 | |- 2 |
|
| 5 | c3 | |- 3 |
|
| 6 | 3 4 5 | ctp | |- { 1 , 2 , 3 } |
| 7 | 1 6 2 | co | |- ( RR ^m { 1 , 2 , 3 } ) |
| 8 | 0 7 | wceq | |- RR3 = ( RR ^m { 1 , 2 , 3 } ) |