Theorem ehlval

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

	Ref	Expression
Hypothesis	ehlval.e	|- E = ( EEhil ` N )
Assertion	ehlval	|- ( N e. NN0 -> E = ( RR^ ` ( 1 ... N ) ) )

Proof

Step	Hyp	Ref	Expression
1		ehlval.e	|- E = ( EEhil ` N )
2		oveq2	|- ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
3	2	fveq2d	|- ( n = N -> ( RR^ ` ( 1 ... n ) ) = ( RR^ ` ( 1 ... N ) ) )
4		df-ehl	|- EEhil = ( n e. NN0 |-> ( RR^ ` ( 1 ... n ) ) )
5		fvex	|- ( RR^ ` ( 1 ... N ) ) e. _V
6	3 4 5	fvmpt	|- ( N e. NN0 -> ( EEhil ` N ) = ( RR^ ` ( 1 ... N ) ) )
7	1 6	eqtrid	|- ( N e. NN0 -> E = ( RR^ ` ( 1 ... N ) ) )