This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ehl0

Description: The Euclidean space of dimension 0 consists of the neutral element only. (Contributed by AV, 12-Feb-2023)

Ref Expression
Hypotheses ehl0base.e 
|- E = ( EEhil ` 0 )
ehl0base.0 
|- .0. = ( 0g ` E )
Assertion ehl0 
|- ( Base ` E ) = { .0. }

Proof

Step Hyp Ref Expression
1 ehl0base.e 
 |-  E = ( EEhil ` 0 )
2 ehl0base.0 
 |-  .0. = ( 0g ` E )
3 1 ehl0base 
 |-  ( Base ` E ) = { (/) }
4 ovex 
 |-  ( 1 ... 0 ) e. _V
5 0nn0 
 |-  0 e. NN0
6 1 ehlval 
 |-  ( 0 e. NN0 -> E = ( RR^ ` ( 1 ... 0 ) ) )
7 5 6 ax-mp 
 |-  E = ( RR^ ` ( 1 ... 0 ) )
8 fz10 
 |-  ( 1 ... 0 ) = (/)
9 8 xpeq1i 
 |-  ( ( 1 ... 0 ) X. { 0 } ) = ( (/) X. { 0 } )
10 9 eqcomi 
 |-  ( (/) X. { 0 } ) = ( ( 1 ... 0 ) X. { 0 } )
11 7 10 rrx0 
 |-  ( ( 1 ... 0 ) e. _V -> ( 0g ` E ) = ( (/) X. { 0 } ) )
12 4 11 ax-mp 
 |-  ( 0g ` E ) = ( (/) X. { 0 } )
13 2 12 eqtri 
 |-  .0. = ( (/) X. { 0 } )
14 0xp 
 |-  ( (/) X. { 0 } ) = (/)
15 13 14 eqtri 
 |-  .0. = (/)
16 15 eqcomi 
 |-  (/) = .0.
17 16 sneqi 
 |-  { (/) } = { .0. }
18 3 17 eqtri 
 |-  ( Base ` E ) = { .0. }