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 𝐻 = ( ℝ^ ‘ 𝐼 )
rrxbase.b 𝐵 = ( Base ‘ 𝐻 )
Assertion rrxip ( 𝐼𝑉 → ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( ℝfld Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) · ( 𝑔𝑥 ) ) ) ) ) = ( ·𝑖𝐻 ) )

Proof

Step Hyp Ref Expression
1 rrxval.r 𝐻 = ( ℝ^ ‘ 𝐼 )
2 rrxbase.b 𝐵 = ( Base ‘ 𝐻 )
3 1 2 rrxprds ( 𝐼𝑉𝐻 = ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) ) )
4 3 fveq2d ( 𝐼𝑉 → ( ·𝑖𝐻 ) = ( ·𝑖 ‘ ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) ) ) )
5 eqid ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) ) = ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) )
6 eqid ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) ) = ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) )
7 5 6 tcphip ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) ) = ( ·𝑖 ‘ ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) ) )
8 2 fvexi 𝐵 ∈ V
9 eqid ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) = ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 )
10 eqid ( ·𝑖 ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) = ( ·𝑖 ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) )
11 9 10 ressip ( 𝐵 ∈ V → ( ·𝑖 ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) = ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) ) )
12 8 11 ax-mp ( ·𝑖 ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) = ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) )
13 eqid ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) = ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) )
14 refld fld ∈ Field
15 14 a1i ( 𝐼𝑉 → ℝfld ∈ Field )
16 snex { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ∈ V
17 xpexg ( ( 𝐼𝑉 ∧ { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ∈ V ) → ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ∈ V )
18 16 17 mpan2 ( 𝐼𝑉 → ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ∈ V )
19 eqid ( Base ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) = ( Base ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) )
20 fvex ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) ∈ V
21 20 snnz { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ≠ ∅
22 dmxp ( { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ≠ ∅ → dom ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) = 𝐼 )
23 21 22 ax-mp dom ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) = 𝐼
24 23 a1i ( 𝐼𝑉 → dom ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) = 𝐼 )
25 13 15 18 19 24 10 prdsip ( 𝐼𝑉 → ( ·𝑖 ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) = ( 𝑓 ∈ ( Base ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) , 𝑔 ∈ ( Base ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) ↦ ( ℝfld Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) )
26 13 15 18 19 24 prdsbas ( 𝐼𝑉 → ( Base ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) = X 𝑥𝐼 ( Base ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) )
27 eqidd ( 𝑥𝐼 → ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) = ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) )
28 rebase ℝ = ( Base ‘ ℝfld )
29 28 eqimssi ℝ ⊆ ( Base ‘ ℝfld )
30 29 a1i ( 𝑥𝐼 → ℝ ⊆ ( Base ‘ ℝfld ) )
31 27 30 srabase ( 𝑥𝐼 → ( Base ‘ ℝfld ) = ( Base ‘ ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) ) )
32 28 a1i ( 𝑥𝐼 → ℝ = ( Base ‘ ℝfld ) )
33 20 fvconst2 ( 𝑥𝐼 → ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) = ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) )
34 33 fveq2d ( 𝑥𝐼 → ( Base ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) = ( Base ‘ ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) ) )
35 31 32 34 3eqtr4rd ( 𝑥𝐼 → ( Base ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) = ℝ )
36 35 adantl ( ( 𝐼𝑉𝑥𝐼 ) → ( Base ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) = ℝ )
37 36 ixpeq2dva ( 𝐼𝑉X 𝑥𝐼 ( Base ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) = X 𝑥𝐼 ℝ )
38 reex ℝ ∈ V
39 ixpconstg ( ( 𝐼𝑉 ∧ ℝ ∈ V ) → X 𝑥𝐼 ℝ = ( ℝ ↑m 𝐼 ) )
40 38 39 mpan2 ( 𝐼𝑉X 𝑥𝐼 ℝ = ( ℝ ↑m 𝐼 ) )
41 26 37 40 3eqtrd ( 𝐼𝑉 → ( Base ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) = ( ℝ ↑m 𝐼 ) )
42 remulr · = ( .r ‘ ℝfld )
43 33 30 sraip ( 𝑥𝐼 → ( .r ‘ ℝfld ) = ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) )
44 42 43 eqtr2id ( 𝑥𝐼 → ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) = · )
45 44 oveqd ( 𝑥𝐼 → ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) ( 𝑔𝑥 ) ) = ( ( 𝑓𝑥 ) · ( 𝑔𝑥 ) ) )
46 45 mpteq2ia ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) ( 𝑔𝑥 ) ) ) = ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) · ( 𝑔𝑥 ) ) )
47 46 a1i ( 𝐼𝑉 → ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) ( 𝑔𝑥 ) ) ) = ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) · ( 𝑔𝑥 ) ) ) )
48 47 oveq2d ( 𝐼𝑉 → ( ℝfld Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) ( 𝑔𝑥 ) ) ) ) = ( ℝfld Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) · ( 𝑔𝑥 ) ) ) ) )
49 41 41 48 mpoeq123dv ( 𝐼𝑉 → ( 𝑓 ∈ ( Base ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) , 𝑔 ∈ ( Base ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) ↦ ( ℝfld Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ‘ 𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( ℝfld Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) · ( 𝑔𝑥 ) ) ) ) ) )
50 25 49 eqtrd ( 𝐼𝑉 → ( ·𝑖 ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( ℝfld Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) · ( 𝑔𝑥 ) ) ) ) ) )
51 12 50 eqtr3id ( 𝐼𝑉 → ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( ℝfld Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) · ( 𝑔𝑥 ) ) ) ) ) )
52 7 51 eqtr3id ( 𝐼𝑉 → ( ·𝑖 ‘ ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( ℝfld Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) · ( 𝑔𝑥 ) ) ) ) ) )
53 4 52 eqtr2d ( 𝐼𝑉 → ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( ℝfld Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) · ( 𝑔𝑥 ) ) ) ) ) = ( ·𝑖𝐻 ) )