Theorem ehlbase

Description: The base of the Euclidean space is the set of n-tuples of real numbers. (Contributed by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypothesis	ehlval.e	$$⊢E={𝔼}_{\mathrm{hil}}\left(N\right)$$
Assertion	ehlbase	$$⊢N\in {\mathbb{N}}_0\to {ℝ}^{\left(0..^N\right)}={\mathrm{Base}}_E$$

Proof

Step	Hyp	Ref	Expression
1		ehlval.e	$$⊢E={𝔼}_{\mathrm{hil}}\left(N\right)$$
2		rabid2	$$⊢{ℝ}^{\left(0..^N\right)}=\left\{f\in \left({ℝ}^{\left(0..^N\right)}\right)|{finSupp}_0\left(f\right)\right\}\leftrightarrow \forall f\in \left({ℝ}^{\left(0..^N\right)}\right){finSupp}_0\left(f\right)$$
3		elmapi	$$⊢f\in \left({ℝ}^{\left(0..^N\right)}\right)\to f:\left(0..^N\right)⟶ℝ$$
4		fzofi	$$⊢\left(0..^N\right)\in \mathrm{Fin}$$
5	4	a1i	$$⊢f\in \left({ℝ}^{\left(0..^N\right)}\right)\to \left(0..^N\right)\in \mathrm{Fin}$$
6		c0ex	$$⊢0\in \mathrm{V}$$
7	6	a1i	$$⊢f\in \left({ℝ}^{\left(0..^N\right)}\right)\to 0\in \mathrm{V}$$
8	3 5 7	fdmfifsupp	$$⊢f\in \left({ℝ}^{\left(0..^N\right)}\right)\to {finSupp}_0\left(f\right)$$
9	2 8	mprgbir	$$⊢{ℝ}^{\left(0..^N\right)}=\left\{f\in \left({ℝ}^{\left(0..^N\right)}\right)|{finSupp}_0\left(f\right)\right\}$$
10		ovex	$$⊢\left(0..^N\right)\in \mathrm{V}$$
11		eqid
12		eqid
13	11 12	rrxbase
14	10 13	ax-mp
15	9 14	eqtr4i
16	1	ehlval
17	16	fveq2d
18	15 17	eqtr4id	$$⊢N\in {\mathbb{N}}_0\to {ℝ}^{\left(0..^N\right)}={\mathrm{Base}}_E$$