This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rrxbasefi

Description: The base of the generalized real Euclidean space, when the dimension of the space is finite. This justifies the use of ( RR ^m X ) for the development of the Lebesgue measure theory for n-dimensional real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses rrxbasefi.x 
|- ( ph -> X e. Fin )
rrxbasefi.h 
|- H = ( RR^ ` X )
rrxbasefi.b 
|- B = ( Base ` H )
Assertion rrxbasefi 
|- ( ph -> B = ( RR ^m X ) )

Proof

Step Hyp Ref Expression
1 rrxbasefi.x 
 |-  ( ph -> X e. Fin )
2 rrxbasefi.h 
 |-  H = ( RR^ ` X )
3 rrxbasefi.b 
 |-  B = ( Base ` H )
4 2 3 rrxbase 
 |-  ( X e. Fin -> B = { f e. ( RR ^m X ) | f finSupp 0 } )
5 1 4 syl 
 |-  ( ph -> B = { f e. ( RR ^m X ) | f finSupp 0 } )
6 ssrab2 
 |-  { f e. ( RR ^m X ) | f finSupp 0 } C_ ( RR ^m X )
7 5 6 eqsstrdi 
 |-  ( ph -> B C_ ( RR ^m X ) )
8 simpr 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> f e. ( RR ^m X ) )
9 elmapi 
 |-  ( f e. ( RR ^m X ) -> f : X --> RR )
10 9 adantl 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> f : X --> RR )
11 1 adantr 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> X e. Fin )
12 c0ex 
 |-  0 e. _V
13 12 a1i 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> 0 e. _V )
14 10 11 13 fdmfifsupp 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> f finSupp 0 )
15 rabid 
 |-  ( f e. { f e. ( RR ^m X ) | f finSupp 0 } <-> ( f e. ( RR ^m X ) /\ f finSupp 0 ) )
16 8 14 15 sylanbrc 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> f e. { f e. ( RR ^m X ) | f finSupp 0 } )
17 5 eqcomd 
 |-  ( ph -> { f e. ( RR ^m X ) | f finSupp 0 } = B )
18 17 adantr 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> { f e. ( RR ^m X ) | f finSupp 0 } = B )
19 16 18 eleqtrd 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> f e. B )
20 7 19 eqelssd 
 |-  ( ph -> B = ( RR ^m X ) )