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

Metamath Proof Explorer

Theorem rrxbase

Description: The base of the generalized real Euclidean space is the set of functions with finite support. (Contributed by Thierry Arnoux, 16-Jun-2019) (Proof shortened by AV, 22-Jul-2019)

Ref Expression
Hypotheses rrxval.r 
|- H = ( RR^ ` I )
rrxbase.b 
|- B = ( Base ` H )
Assertion rrxbase 
|- ( I e. V -> B = { f e. ( RR ^m I ) | f finSupp 0 } )

Proof

Step Hyp Ref Expression
1 rrxval.r 
 |-  H = ( RR^ ` I )
2 rrxbase.b 
 |-  B = ( Base ` H )
3 1 rrxval 
 |-  ( I e. V -> H = ( toCPreHil ` ( RRfld freeLMod I ) ) )
4 3 fveq2d 
 |-  ( I e. V -> ( Base ` H ) = ( Base ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
5 eqid 
 |-  ( toCPreHil ` ( RRfld freeLMod I ) ) = ( toCPreHil ` ( RRfld freeLMod I ) )
6 eqid 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( RRfld freeLMod I ) )
7 5 6 tcphbas 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
8 4 7 eqtr4di 
 |-  ( I e. V -> ( Base ` H ) = ( Base ` ( RRfld freeLMod I ) ) )
9 2 a1i 
 |-  ( I e. V -> B = ( Base ` H ) )
10 refld 
 |-  RRfld e. Field
11 eqid 
 |-  ( RRfld freeLMod I ) = ( RRfld freeLMod I )
12 rebase 
 |-  RR = ( Base ` RRfld )
13 re0g 
 |-  0 = ( 0g ` RRfld )
14 eqid 
 |-  { f e. ( RR ^m I ) | f finSupp 0 } = { f e. ( RR ^m I ) | f finSupp 0 }
15 11 12 13 14 frlmbas 
 |-  ( ( RRfld e. Field /\ I e. V ) -> { f e. ( RR ^m I ) | f finSupp 0 } = ( Base ` ( RRfld freeLMod I ) ) )
16 10 15 mpan 
 |-  ( I e. V -> { f e. ( RR ^m I ) | f finSupp 0 } = ( Base ` ( RRfld freeLMod I ) ) )
17 8 9 16 3eqtr4d 
 |-  ( I e. V -> B = { f e. ( RR ^m I ) | f finSupp 0 } )