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 = msup$

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 msup = msup$
4		df-ehl	$⊢ 𝔼_{hil} = (n \in ℕ_{0} ⟼ msup)$
5		fvex	$⊢ msup \in V$
6	3 4 5	fvmpt	$⊢ N \in ℕ_{0} \to 𝔼_{hil} (N) = msup$
7	1 6	eqtrid	$⊢ N \in ℕ_{0} \to E = msup$