Metamath Proof Explorer

Theorem ehlval

Description: Value of the Euclidean space of dimension N . (Contributed by Thierry Arnoux, 16-Jun-2019)

		Ref	Expression
	Hypothesis	ehlval.e	$⊢ E = 𝔼_{hil} (N)$
	Assertion	ehlval	$⊢ N \in ℕ_{0} \to E = (1 \dots N)$

Step	Hyp	Ref	Expression
1		ehlval.e	$⊢ E = 𝔼_{hil} (N)$
2		oveq2	$⊢ n = N \to (1 \dots n) = (1 \dots N)$
3	2	fveq2d	$⊢ n = N \to (1 \dots n) = (1 \dots N)$
4		df-ehl	$⊢ 𝔼_{hil} = (n \in ℕ_{0} ⟼ (1 \dots n))$
5		fvex	$⊢ (1 \dots N) \in V$
6	3 4 5	fvmpt	$⊢ N \in ℕ_{0} \to 𝔼_{hil} (N) = (1 \dots N)$
7	1 6	syl5eq	$⊢ N \in ℕ_{0} \to E = (1 \dots N)$