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

Proof

Step	Hyp	Ref	Expression
1		ehl0base.e	$$⊢E={𝔼}_{\mathrm{hil}}\left(0\right)$$
2		ehl0base.0	$$⊢\underset{\dot{}}{0}=0_E$$
3	1	ehl0base	$$⊢{\mathrm{Base}}_E=\left\{\varnothing \right\}$$
4		ovex	$$⊢\left(1\dots 0\right)\in \mathrm{V}$$
5		0nn0	$$⊢0\in {\mathbb{N}}_0$$
6	1	ehlval	$$⊢0\in {\mathbb{N}}_0\to E={\mathrm{<mfenced><mrow><mn>\; 1\; </mn>\; <mo\; href="df-fz.html">\dots </mo>\; <mn>\; 0\; </mn></mrow></mfenced>}}^{}$$
7	5 6	ax-mp	$$⊢E={\mathrm{<mfenced><mrow><mn>\; 1\; </mn>\; <mo\; href="df-fz.html">\dots </mo>\; <mn>\; 0\; </mn></mrow></mfenced>}}^{}$$
8		fz10	$$⊢\left(1\dots 0\right)=\varnothing$$
9	8	xpeq1i	$$⊢\left(1\dots 0\right)\times \left\{0\right\}=\varnothing \times \left\{0\right\}$$
10	9	eqcomi	$$⊢\varnothing \times \left\{0\right\}=\left(1\dots 0\right)\times \left\{0\right\}$$
11	7 10	rrx0	$$⊢\left(1\dots 0\right)\in \mathrm{V}\to 0_E=\varnothing \times \left\{0\right\}$$
12	4 11	ax-mp	$$⊢0_E=\varnothing \times \left\{0\right\}$$
13	2 12	eqtri	$$⊢\underset{\dot{}}{0}=\varnothing \times \left\{0\right\}$$
14		0xp	$$⊢\varnothing \times \left\{0\right\}=\varnothing$$
15	13 14	eqtri	$$⊢\underset{\dot{}}{0}=\varnothing$$
16	15	eqcomi	$$⊢\varnothing =\underset{\dot{}}{0}$$
17	16	sneqi	$$⊢\left\{\varnothing \right\}=\left\{\underset{\dot{}}{0}\right\}$$
18	3 17	eqtri	$$⊢{\mathrm{Base}}_E=\left\{\underset{\dot{}}{0}\right\}$$