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. }