Theorem ehlval

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

	Ref	Expression
Hypothesis	ehlval.e	⊢ 𝐸 = ( 𝔼hil ‘ 𝑁 )
Assertion	ehlval	⊢ ( 𝑁 ∈ ℕ0 → 𝐸 = ( ℝ^ ‘ ( 1 ... 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ehlval.e	⊢ 𝐸 = ( 𝔼hil ‘ 𝑁 )
2		oveq2	⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
3	2	fveq2d	⊢ ( 𝑛 = 𝑁 → ( ℝ^ ‘ ( 1 ... 𝑛 ) ) = ( ℝ^ ‘ ( 1 ... 𝑁 ) ) )
4		df-ehl	⊢ 𝔼hil = ( 𝑛 ∈ ℕ0 ↦ ( ℝ^ ‘ ( 1 ... 𝑛 ) ) )
5		fvex	⊢ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ∈ V
6	3 4 5	fvmpt	⊢ ( 𝑁 ∈ ℕ0 → ( 𝔼hil ‘ 𝑁 ) = ( ℝ^ ‘ ( 1 ... 𝑁 ) ) )
7	1 6	syl5eq	⊢ ( 𝑁 ∈ ℕ0 → 𝐸 = ( ℝ^ ‘ ( 1 ... 𝑁 ) ) )