Metamath Proof Explorer

Theorem dipfval

Description: The inner product function on a normed complex vector space. The definition is meaningful for vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law. (Contributed by NM, 10-Apr-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses dipfval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
dipfval.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
dipfval.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
dipfval.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
dipfval.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
Assertion dipfval ( 𝑈 ∈ NrmCVec → 𝑃 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) )

Proof

Step Hyp Ref Expression
1 dipfval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 dipfval.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 dipfval.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 dipfval.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
5 dipfval.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
6 fveq2 ⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = ( BaseSet ‘ 𝑈 ) )
7 6 1 eqtr4di ⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = 𝑋 )
8 fveq2 ⊢ ( 𝑢 = 𝑈 → ( normCV ‘ 𝑢 ) = ( normCV ‘ 𝑈 ) )
9 8 4 eqtr4di ⊢ ( 𝑢 = 𝑈 → ( normCV ‘ 𝑢 ) = 𝑁 )
10 fveq2 ⊢ ( 𝑢 = 𝑈 → ( +𝑣 ‘ 𝑢 ) = ( +𝑣 ‘ 𝑈 ) )
11 10 2 eqtr4di ⊢ ( 𝑢 = 𝑈 → ( +𝑣 ‘ 𝑢 ) = 𝐺 )
12 eqidd ⊢ ( 𝑢 = 𝑈 → 𝑥 = 𝑥 )
13 fveq2 ⊢ ( 𝑢 = 𝑈 → ( ·𝑠OLD ‘ 𝑢 ) = ( ·𝑠OLD ‘ 𝑈 ) )
14 13 3 eqtr4di ⊢ ( 𝑢 = 𝑈 → ( ·𝑠OLD ‘ 𝑢 ) = 𝑆 )
15 14 oveqd ⊢ ( 𝑢 = 𝑈 → ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) = ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) )
16 11 12 15 oveq123d ⊢ ( 𝑢 = 𝑈 → ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) = ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) )
17 9 16 fveq12d ⊢ ( 𝑢 = 𝑈 → ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) = ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) )
18 17 oveq1d ⊢ ( 𝑢 = 𝑈 → ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) )
19 18 oveq2d ⊢ ( 𝑢 = 𝑈 → ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) ) = ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) )
20 19 sumeq2sdv ⊢ ( 𝑢 = 𝑈 → Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) ) = Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) )
21 20 oveq1d ⊢ ( 𝑢 = 𝑈 → ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) )
22 7 7 21 mpoeq123dv ⊢ ( 𝑢 = 𝑈 → ( 𝑥 ∈ ( BaseSet ‘ 𝑢 ) , 𝑦 ∈ ( BaseSet ‘ 𝑢 ) ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) )
23 df-dip ⊢ ·𝑖OLD = ( 𝑢 ∈ NrmCVec ↦ ( 𝑥 ∈ ( BaseSet ‘ 𝑢 ) , 𝑦 ∈ ( BaseSet ‘ 𝑢 ) ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) )
24 1 fvexi ⊢ 𝑋 ∈ V
25 24 24 mpoex ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) ∈ V
26 22 23 25 fvmpt ⊢ ( 𝑈 ∈ NrmCVec → ( ·𝑖OLD ‘ 𝑈 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) )
27 5 26 syl5eq ⊢ ( 𝑈 ∈ NrmCVec → 𝑃 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) )