Theorem ehlbase

Description: The base of the Euclidean space is the set of n-tuples of real numbers. (Contributed by Thierry Arnoux, 16-Jun-2019)

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

Proof

Step	Hyp	Ref	Expression
1		ehlval.e	|- E = ( EEhil ` N )
2		rabid2	|- ( ( RR ^m ( 0 ..^ N ) ) = { f e. ( RR ^m ( 0 ..^ N ) ) | f finSupp 0 } <-> A. f e. ( RR ^m ( 0 ..^ N ) ) f finSupp 0 )
3		elmapi	|- ( f e. ( RR ^m ( 0 ..^ N ) ) -> f : ( 0 ..^ N ) --> RR )
4		fzofi	|- ( 0 ..^ N ) e. Fin
5	4	a1i	|- ( f e. ( RR ^m ( 0 ..^ N ) ) -> ( 0 ..^ N ) e. Fin )
6		c0ex	|- 0 e. _V
7	6	a1i	|- ( f e. ( RR ^m ( 0 ..^ N ) ) -> 0 e. _V )
8	3 5 7	fdmfifsupp	|- ( f e. ( RR ^m ( 0 ..^ N ) ) -> f finSupp 0 )
9	2 8	mprgbir	|- ( RR ^m ( 0 ..^ N ) ) = { f e. ( RR ^m ( 0 ..^ N ) ) | f finSupp 0 }
10		ovex	|- ( 0 ..^ N ) e. _V
11		eqid	|- ( RR^ ` ( 0 ..^ N ) ) = ( RR^ ` ( 0 ..^ N ) )
12		eqid	|- ( Base ` ( RR^ ` ( 0 ..^ N ) ) ) = ( Base ` ( RR^ ` ( 0 ..^ N ) ) )
13	11 12	rrxbase	|- ( ( 0 ..^ N ) e. _V -> ( Base ` ( RR^ ` ( 0 ..^ N ) ) ) = { f e. ( RR ^m ( 0 ..^ N ) ) | f finSupp 0 } )
14	10 13	ax-mp	|- ( Base ` ( RR^ ` ( 0 ..^ N ) ) ) = { f e. ( RR ^m ( 0 ..^ N ) ) | f finSupp 0 }
15	9 14	eqtr4i	|- ( RR ^m ( 0 ..^ N ) ) = ( Base ` ( RR^ ` ( 0 ..^ N ) ) )
16	1	ehlval	|- ( N e. NN0 -> E = ( RR^ ` ( 0 ..^ N ) ) )
17	16	fveq2d	|- ( N e. NN0 -> ( Base ` E ) = ( Base ` ( RR^ ` ( 0 ..^ N ) ) ) )
18	15 17	eqtr4id	|- ( N e. NN0 -> ( RR ^m ( 0 ..^ N ) ) = ( Base ` E ) )