Metamath Proof Explorer

Theorem ipval

Description: Value of the inner product. The definition is meaningful for normed complex vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law, although for convenience we define it for any normed complex vector space. The vector (group) addition operation is G , the scalar product is S , the norm is N , and the set of vectors is X . Equation 6.45 of Ponnusamy p. 361. (Contributed by NM, 31-Jan-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 ipval ( ( 𝑈 ∈ 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 1 2 3 4 5 dipfval ⊢ ( 𝑈 ∈ NrmCVec → 𝑃 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) )
7 6 oveqd ⊢ ( 𝑈 ∈ NrmCVec → ( 𝐴 𝑃 𝐵 ) = ( 𝐴 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) 𝐵 ) )
8 fvoveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) )
9 8 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) )
10 9 oveq2d ⊢ ( 𝑥 = 𝐴 → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) )
11 10 sumeq2sdv ⊢ ( 𝑥 = 𝐴 → Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) = Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) )
12 11 oveq1d ⊢ ( 𝑥 = 𝐴 → ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) )
13 oveq2 ⊢ ( 𝑦 = 𝐵 → ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) = ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) )
14 13 oveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) = ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) )
15 14 fveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) )
16 15 oveq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) )
17 16 oveq2d ⊢ ( 𝑦 = 𝐵 → ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) = ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
18 17 sumeq2sdv ⊢ ( 𝑦 = 𝐵 → Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) = Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) )
19 18 oveq1d ⊢ ( 𝑦 = 𝐵 → ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) / 4 ) )
20 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) )
21 ovex ⊢ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) / 4 ) ∈ V
22 12 19 20 21 ovmpo ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝑥 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) 𝐵 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) / 4 ) )
23 7 22 sylan9eq ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝑃 𝐵 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) / 4 ) )
24 23 3impb ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( ( i ↑ 𝑘 ) 𝑆 𝐵 ) ) ) ↑ 2 ) ) / 4 ) )