Metamath Proof Explorer

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 ( 1 ... N ) ) = ( Base ` E ) )

Proof

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