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	⊢ 𝐸 = ( 𝔼hil ‘ 0 )
Assertion	ehl0base	⊢ ( Base ‘ 𝐸 ) = { ∅ }

Proof

Step	Hyp	Ref	Expression
1		ehl0base.e	⊢ 𝐸 = ( 𝔼hil ‘ 0 )
2		0nn0	⊢ 0 ∈ ℕ0
3	1	ehlbase	⊢ ( 0 ∈ ℕ0 → ( ℝ ↑m ( 1 ... 0 ) ) = ( Base ‘ 𝐸 ) )
4	3	eqcomd	⊢ ( 0 ∈ ℕ0 → ( Base ‘ 𝐸 ) = ( ℝ ↑m ( 1 ... 0 ) ) )
5	2 4	ax-mp	⊢ ( Base ‘ 𝐸 ) = ( ℝ ↑m ( 1 ... 0 ) )
6		fz10	⊢ ( 1 ... 0 ) = ∅
7	6	oveq2i	⊢ ( ℝ ↑m ( 1 ... 0 ) ) = ( ℝ ↑m ∅ )
8		reex	⊢ ℝ ∈ V
9		mapdm0	⊢ ( ℝ ∈ V → ( ℝ ↑m ∅ ) = { ∅ } )
10	8 9	ax-mp	⊢ ( ℝ ↑m ∅ ) = { ∅ }
11	5 7 10	3eqtri	⊢ ( Base ‘ 𝐸 ) = { ∅ }