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	1	ehlval	$⊢ N \in ℕ_{0} \to E = (1 \dots N)$
3	2	fveq2d	$⊢ N \in ℕ_{0} \to {Base}_{E} = {Base}_{(1 \dots N)}$
4		rabid2	$⊢ ℝ^{(1 \dots N)} = \{f \in (ℝ^{(1 \dots N)}) \| {finSupp}_{0} (f)\} \leftrightarrow \forall f \in (ℝ^{(1 \dots N)}) {finSupp}_{0} (f)$
5		elmapi	$⊢ f \in (ℝ^{(1 \dots N)}) \to f : (1 \dots N) ⟶ ℝ$
6		fzfid	$⊢ f \in (ℝ^{(1 \dots N)}) \to (1 \dots N) \in Fin$
7		0red	$⊢ f \in (ℝ^{(1 \dots N)}) \to 0 \in ℝ$
8	5 6 7	fdmfifsupp	$⊢ f \in (ℝ^{(1 \dots N)}) \to {finSupp}_{0} (f)$
9	4 8	mprgbir	$⊢ ℝ^{(1 \dots N)} = \{f \in (ℝ^{(1 \dots N)}) \| {finSupp}_{0} (f)\}$
10		ovex	$⊢ (1 \dots N) \in V$
11		eqid	$⊢ (1 \dots N) = (1 \dots N)$
12		eqid	$⊢ {Base}_{(1 \dots N)} = {Base}_{(1 \dots N)}$
13	11 12	rrxbase	$⊢ (1 \dots N) \in V \to {Base}_{(1 \dots N)} = \{f \in (ℝ^{(1 \dots N)}) \| {finSupp}_{0} (f)\}$
14	10 13	ax-mp	$⊢ {Base}_{(1 \dots N)} = \{f \in (ℝ^{(1 \dots N)}) \| {finSupp}_{0} (f)\}$
15	9 14	eqtr4i	$⊢ ℝ^{(1 \dots N)} = {Base}_{(1 \dots N)}$
16	3 15	syl6reqr	$⊢ N \in ℕ_{0} \to ℝ^{(1 \dots N)} = {Base}_{E}$

Metamath Proof Explorer