Metamath Proof Explorer

Theorem rrxval

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

Ref Expression
Hypothesis rrxval.r 
|- H = ( RR^ ` I )
Assertion rrxval 
|- ( I e. V -> H = ( toCPreHil ` ( RRfld freeLMod I ) ) )

Proof

Step Hyp Ref Expression
1 rrxval.r 
 |-  H = ( RR^ ` I )
2 elex 
 |-  ( I e. V -> I e. _V )
3 oveq2 
 |-  ( i = I -> ( RRfld freeLMod i ) = ( RRfld freeLMod I ) )
4 3 fveq2d 
 |-  ( i = I -> ( toCPreHil ` ( RRfld freeLMod i ) ) = ( toCPreHil ` ( RRfld freeLMod I ) ) )
5 df-rrx 
 |-  RR^ = ( i e. _V |-> ( toCPreHil ` ( RRfld freeLMod i ) ) )
6 fvex 
 |-  ( toCPreHil ` ( RRfld freeLMod I ) ) e. _V
7 4 5 6 fvmpt 
 |-  ( I e. _V -> ( RR^ ` I ) = ( toCPreHil ` ( RRfld freeLMod I ) ) )
8 2 7 syl 
 |-  ( I e. V -> ( RR^ ` I ) = ( toCPreHil ` ( RRfld freeLMod I ) ) )
9 1 8 eqtrid 
 |-  ( I e. V -> H = ( toCPreHil ` ( RRfld freeLMod I ) ) )