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 = 𝔼_{hil} (0)$
	Assertion	ehl0base	$⊢ {Base}_{E} = \{\emptyset\}$

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

Metamath Proof Explorer