Description: The base of the Euclidean space of dimension 0 consists only of one element, the empty set. (Contributed by AV, 12-Feb-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ehl0base.e | |- E = ( EEhil ` 0 ) |
|
| Assertion | ehl0base | |- ( Base ` E ) = { (/) } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ehl0base.e | |- E = ( EEhil ` 0 ) |
|
| 2 | 0nn0 | |- 0 e. NN0 |
|
| 3 | 1 | ehlbase | |- ( 0 e. NN0 -> ( RR ^m ( 1 ... 0 ) ) = ( Base ` E ) ) |
| 4 | 3 | eqcomd | |- ( 0 e. NN0 -> ( Base ` E ) = ( RR ^m ( 1 ... 0 ) ) ) |
| 5 | 2 4 | ax-mp | |- ( Base ` E ) = ( RR ^m ( 1 ... 0 ) ) |
| 6 | fz10 | |- ( 1 ... 0 ) = (/) |
|
| 7 | 6 | oveq2i | |- ( RR ^m ( 1 ... 0 ) ) = ( RR ^m (/) ) |
| 8 | reex | |- RR e. _V |
|
| 9 | mapdm0 | |- ( RR e. _V -> ( RR ^m (/) ) = { (/) } ) |
|
| 10 | 8 9 | ax-mp | |- ( RR ^m (/) ) = { (/) } |
| 11 | 5 7 10 | 3eqtri | |- ( Base ` E ) = { (/) } |