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 = 𝔼_{hil} (N)$
	Assertion	ehlbase	$⊢ N \in ℕ_{0} \to ℝ^{(1 \dots N)} = {Base}_{E}$

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

Metamath Proof Explorer