Metamath Proof Explorer

Theorem rrxprds

Description: Expand the definition of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypotheses rrxval.r 
|- H = ( RR^ ` I )
rrxbase.b 
|- B = ( Base ` H )
Assertion rrxprds 
|- ( I e. V -> H = ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) ) )

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 refld 
 |-  RRfld e. Field
5 eqid 
 |-  ( RRfld freeLMod I ) = ( RRfld freeLMod I )
6 eqid 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( RRfld freeLMod I ) )
7 5 6 frlmpws 
 |-  ( ( RRfld e. Field /\ I e. V ) -> ( RRfld freeLMod I ) = ( ( ( ringLMod ` RRfld ) ^s I ) |`s ( Base ` ( RRfld freeLMod I ) ) ) )
8 4 7 mpan 
 |-  ( I e. V -> ( RRfld freeLMod I ) = ( ( ( ringLMod ` RRfld ) ^s I ) |`s ( Base ` ( RRfld freeLMod I ) ) ) )
9 fvex 
 |-  ( ( subringAlg ` RRfld ) ` RR ) e. _V
10 rlmval 
 |-  ( ringLMod ` RRfld ) = ( ( subringAlg ` RRfld ) ` ( Base ` RRfld ) )
11 rebase 
 |-  RR = ( Base ` RRfld )
12 11 fveq2i 
 |-  ( ( subringAlg ` RRfld ) ` RR ) = ( ( subringAlg ` RRfld ) ` ( Base ` RRfld ) )
13 10 12 eqtr4i 
 |-  ( ringLMod ` RRfld ) = ( ( subringAlg ` RRfld ) ` RR )
14 13 oveq1i 
 |-  ( ( ringLMod ` RRfld ) ^s I ) = ( ( ( subringAlg ` RRfld ) ` RR ) ^s I )
15 11 ressid 
 |-  ( RRfld e. Field -> ( RRfld |`s RR ) = RRfld )
16 4 15 ax-mp 
 |-  ( RRfld |`s RR ) = RRfld
17 eqidd 
 |-  ( T. -> ( ( subringAlg ` RRfld ) ` RR ) = ( ( subringAlg ` RRfld ) ` RR ) )
18 11 eqimssi 
 |-  RR C_ ( Base ` RRfld )
19 18 a1i 
 |-  ( T. -> RR C_ ( Base ` RRfld ) )
20 17 19 srasca 
 |-  ( T. -> ( RRfld |`s RR ) = ( Scalar ` ( ( subringAlg ` RRfld ) ` RR ) ) )
21 20 mptru 
 |-  ( RRfld |`s RR ) = ( Scalar ` ( ( subringAlg ` RRfld ) ` RR ) )
22 16 21 eqtr3i 
 |-  RRfld = ( Scalar ` ( ( subringAlg ` RRfld ) ` RR ) )
23 14 22 pwsval 
 |-  ( ( ( ( subringAlg ` RRfld ) ` RR ) e. _V /\ I e. V ) -> ( ( ringLMod ` RRfld ) ^s I ) = ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) )
24 9 23 mpan 
 |-  ( I e. V -> ( ( ringLMod ` RRfld ) ^s I ) = ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) )
25 24 eqcomd 
 |-  ( I e. V -> ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) = ( ( ringLMod ` RRfld ) ^s I ) )
26 3 fveq2d 
 |-  ( I e. V -> ( Base ` H ) = ( Base ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
27 eqid 
 |-  ( toCPreHil ` ( RRfld freeLMod I ) ) = ( toCPreHil ` ( RRfld freeLMod I ) )
28 27 6 tcphbas 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
29 26 2 28 3eqtr4g 
 |-  ( I e. V -> B = ( Base ` ( RRfld freeLMod I ) ) )
30 25 29 oveq12d 
 |-  ( I e. V -> ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) = ( ( ( ringLMod ` RRfld ) ^s I ) |`s ( Base ` ( RRfld freeLMod I ) ) ) )
31 8 30 eqtr4d 
 |-  ( I e. V -> ( RRfld freeLMod I ) = ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) )
32 31 fveq2d 
 |-  ( I e. V -> ( toCPreHil ` ( RRfld freeLMod I ) ) = ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) ) )
33 3 32 eqtrd 
 |-  ( I e. V -> H = ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) ) )