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 ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( ·𝑖 ‘ 𝐻 ) )