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 = (0 ..^N)$

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