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(1\dots N\right)}={\mathrm{Base}}_E$$

Proof

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