ehl0

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

Step	Hyp	Ref	Expression
1		ehl0base.e	$⊢ E = 𝔼_{hil} (0)$
2		ehl0base.0	$⊢ \underset{˙}{0} = 0_{E}$
3	1	ehl0base	$⊢ {Base}_{E} = \{\emptyset\}$
4		ovex	$⊢ (1 \dots 0) \in V$
5		0nn0	$⊢ 0 \in ℕ_{0}$
6	1	ehlval	$⊢ 0 \in ℕ_{0} \to E = (1 \dots 0)$
7	5 6	ax-mp	$⊢ E = (1 \dots 0)$
8		fz10	$⊢ (1 \dots 0) = \emptyset$
9	8	xpeq1i	$⊢ (1 \dots 0) \times \{0\} = \emptyset \times \{0\}$
10	9	eqcomi	$⊢ \emptyset \times \{0\} = (1 \dots 0) \times \{0\}$
11	7 10	rrx0	$⊢ (1 \dots 0) \in V \to 0_{E} = \emptyset \times \{0\}$
12	4 11	ax-mp	$⊢ 0_{E} = \emptyset \times \{0\}$
13	2 12	eqtri	$⊢ \underset{˙}{0} = \emptyset \times \{0\}$
14		0xp	$⊢ \emptyset \times \{0\} = \emptyset$
15	13 14	eqtri	$⊢ \underset{˙}{0} = \emptyset$
16	15	eqcomi	$⊢ \emptyset = \underset{˙}{0}$
17	16	sneqi	$⊢ \{\emptyset\} = \{\underset{˙}{0}\}$
18	3 17	eqtri	$⊢ {Base}_{E} = \{\underset{˙}{0}\}$

Metamath Proof Explorer