Metamath Proof Explorer

Theorem rrxip

Description: The inner product 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 rrxip 
|- ( I e. V -> ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( RRfld gsum ( x e. I |-> ( ( f ` x ) x. ( g ` x ) ) ) ) ) = ( .i ` H ) )

Proof

Step Hyp Ref Expression
1 rrxval.r 
 |-  H = ( RR^ ` I )
2 rrxbase.b 
 |-  B = ( Base ` H )
3 1 2 rrxprds 
 |-  ( I e. V -> H = ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) ) )
4 3 fveq2d 
 |-  ( I e. V -> ( .i ` H ) = ( .i ` ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) ) ) )
5 eqid 
 |-  ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) ) = ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) )
6 eqid 
 |-  ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) ) = ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) )
7 5 6 tcphip 
 |-  ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) ) = ( .i ` ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) ) )
8 2 fvexi 
 |-  B e. _V
9 eqid 
 |-  ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) = ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B )
10 eqid 
 |-  ( .i ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) = ( .i ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) )
11 9 10 ressip 
 |-  ( B e. _V -> ( .i ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) = ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) ) )
12 8 11 ax-mp 
 |-  ( .i ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) = ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) )
13 eqid 
 |-  ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) = ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) )
14 refld 
 |-  RRfld e. Field
15 14 a1i 
 |-  ( I e. V -> RRfld e. Field )
16 snex 
 |-  { ( ( subringAlg ` RRfld ) ` RR ) } e. _V
17 xpexg 
 |-  ( ( I e. V /\ { ( ( subringAlg ` RRfld ) ` RR ) } e. _V ) -> ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) e. _V )
18 16 17 mpan2 
 |-  ( I e. V -> ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) e. _V )
19 eqid 
 |-  ( Base ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) = ( Base ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) )
20 fvex 
 |-  ( ( subringAlg ` RRfld ) ` RR ) e. _V
21 20 snnz 
 |-  { ( ( subringAlg ` RRfld ) ` RR ) } =/= (/)
22 dmxp 
 |-  ( { ( ( subringAlg ` RRfld ) ` RR ) } =/= (/) -> dom ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) = I )
23 21 22 ax-mp 
 |-  dom ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) = I
24 23 a1i 
 |-  ( I e. V -> dom ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) = I )
25 13 15 18 19 24 10 prdsip 
 |-  ( I e. V -> ( .i ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) = ( f e. ( Base ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) , g e. ( Base ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) |-> ( RRfld gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) ( g ` x ) ) ) ) ) )
26 13 15 18 19 24 prdsbas 
 |-  ( I e. V -> ( Base ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) = X_ x e. I ( Base ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) )
27 eqidd 
 |-  ( x e. I -> ( ( subringAlg ` RRfld ) ` RR ) = ( ( subringAlg ` RRfld ) ` RR ) )
28 rebase 
 |-  RR = ( Base ` RRfld )
29 28 eqimssi 
 |-  RR C_ ( Base ` RRfld )
30 29 a1i 
 |-  ( x e. I -> RR C_ ( Base ` RRfld ) )
31 27 30 srabase 
 |-  ( x e. I -> ( Base ` RRfld ) = ( Base ` ( ( subringAlg ` RRfld ) ` RR ) ) )
32 28 a1i 
 |-  ( x e. I -> RR = ( Base ` RRfld ) )
33 20 fvconst2 
 |-  ( x e. I -> ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) = ( ( subringAlg ` RRfld ) ` RR ) )
34 33 fveq2d 
 |-  ( x e. I -> ( Base ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) = ( Base ` ( ( subringAlg ` RRfld ) ` RR ) ) )
35 31 32 34 3eqtr4rd 
 |-  ( x e. I -> ( Base ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) = RR )
36 35 adantl 
 |-  ( ( I e. V /\ x e. I ) -> ( Base ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) = RR )
37 36 ixpeq2dva 
 |-  ( I e. V -> X_ x e. I ( Base ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) = X_ x e. I RR )
38 reex 
 |-  RR e. _V
39 ixpconstg 
 |-  ( ( I e. V /\ RR e. _V ) -> X_ x e. I RR = ( RR ^m I ) )
40 38 39 mpan2 
 |-  ( I e. V -> X_ x e. I RR = ( RR ^m I ) )
41 26 37 40 3eqtrd 
 |-  ( I e. V -> ( Base ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) = ( RR ^m I ) )
42 remulr 
 |-  x. = ( .r ` RRfld )
43 33 30 sraip 
 |-  ( x e. I -> ( .r ` RRfld ) = ( .i ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) )
44 42 43 syl5req 
 |-  ( x e. I -> ( .i ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) = x. )
45 44 oveqd 
 |-  ( x e. I -> ( ( f ` x ) ( .i ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) ( g ` x ) ) = ( ( f ` x ) x. ( g ` x ) ) )
46 45 mpteq2ia 
 |-  ( x e. I |-> ( ( f ` x ) ( .i ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) x. ( g ` x ) ) )
47 46 a1i 
 |-  ( I e. V -> ( x e. I |-> ( ( f ` x ) ( .i ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) x. ( g ` x ) ) ) )
48 47 oveq2d 
 |-  ( I e. V -> ( RRfld gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) ( g ` x ) ) ) ) = ( RRfld gsum ( x e. I |-> ( ( f ` x ) x. ( g ` x ) ) ) ) )
49 41 41 48 mpoeq123dv 
 |-  ( I e. V -> ( f e. ( Base ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) , g e. ( Base ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) |-> ( RRfld gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ` x ) ) ( g ` x ) ) ) ) ) = ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( RRfld gsum ( x e. I |-> ( ( f ` x ) x. ( g ` x ) ) ) ) ) )
50 25 49 eqtrd 
 |-  ( I e. V -> ( .i ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) = ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( RRfld gsum ( x e. I |-> ( ( f ` x ) x. ( g ` x ) ) ) ) ) )
51 12 50 eqtr3id 
 |-  ( I e. V -> ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) ) = ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( RRfld gsum ( x e. I |-> ( ( f ` x ) x. ( g ` x ) ) ) ) ) )
52 7 51 eqtr3id 
 |-  ( I e. V -> ( .i ` ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s B ) ) ) = ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( RRfld gsum ( x e. I |-> ( ( f ` x ) x. ( g ` x ) ) ) ) ) )
53 4 52 eqtr2d 
 |-  ( I e. V -> ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( RRfld gsum ( x e. I |-> ( ( f ` x ) x. ( g ` x ) ) ) ) ) = ( .i ` H ) )