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 eqtr2id
 |-  ( 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 ) )