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 = I
rrxbase.b B = Base H
Assertion rrxip I V f I , g I fld x I f x g x = 𝑖 H

Proof

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