Theorem ehl0base

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={𝔼}_{\mathrm{hil}}\left(0\right)$$
Assertion	ehl0base	$$⊢{\mathrm{Base}}_E=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		ehl0base.e	$$⊢E={𝔼}_{\mathrm{hil}}\left(0\right)$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3	1	ehlbase	$$⊢0\in {\mathbb{N}}_0\to {ℝ}^{\left(1\dots 0\right)}={\mathrm{Base}}_E$$
4	3	eqcomd	$$⊢0\in {\mathbb{N}}_0\to {\mathrm{Base}}_E={ℝ}^{\left(1\dots 0\right)}$$
5	2 4	ax-mp	$$⊢{\mathrm{Base}}_E={ℝ}^{\left(1\dots 0\right)}$$
6		fz10	$$⊢\left(1\dots 0\right)=\varnothing$$
7	6	oveq2i	$$⊢{ℝ}^{\left(1\dots 0\right)}={ℝ}^{\varnothing }$$
8		reex	$$⊢ℝ\in \mathrm{V}$$
9		mapdm0	$$⊢ℝ\in \mathrm{V}\to {ℝ}^{\varnothing }=\left\{\varnothing \right\}$$
10	8 9	ax-mp	$$⊢{ℝ}^{\varnothing }=\left\{\varnothing \right\}$$
11	5 7 10	3eqtri	$$⊢{\mathrm{Base}}_E=\left\{\varnothing \right\}$$