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 
|- X = ( BaseSet ` U )
dipfval.2 
|- G = ( +v ` U )
dipfval.4 
|- S = ( .sOLD ` U )
dipfval.6 
|- N = ( normCV ` U )
dipfval.7 
|- P = ( .iOLD ` U )
Assertion dipfval 
|- ( U e. NrmCVec -> P = ( x e. X , y e. X |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( x G ( ( _i ^ k ) S y ) ) ) ^ 2 ) ) / 4 ) ) )

Proof

Step Hyp Ref Expression
1 dipfval.1 
 |-  X = ( BaseSet ` U )
2 dipfval.2 
 |-  G = ( +v ` U )
3 dipfval.4 
 |-  S = ( .sOLD ` U )
4 dipfval.6 
 |-  N = ( normCV ` U )
5 dipfval.7 
 |-  P = ( .iOLD ` U )
6 fveq2 
 |-  ( u = U -> ( BaseSet ` u ) = ( BaseSet ` U ) )
7 6 1 eqtr4di 
 |-  ( u = U -> ( BaseSet ` u ) = X )
8 fveq2 
 |-  ( u = U -> ( normCV ` u ) = ( normCV ` U ) )
9 8 4 eqtr4di 
 |-  ( u = U -> ( normCV ` u ) = N )
10 fveq2 
 |-  ( u = U -> ( +v ` u ) = ( +v ` U ) )
11 10 2 eqtr4di 
 |-  ( u = U -> ( +v ` u ) = G )
12 eqidd 
 |-  ( u = U -> x = x )
13 fveq2 
 |-  ( u = U -> ( .sOLD ` u ) = ( .sOLD ` U ) )
14 13 3 eqtr4di 
 |-  ( u = U -> ( .sOLD ` u ) = S )
15 14 oveqd 
 |-  ( u = U -> ( ( _i ^ k ) ( .sOLD ` u ) y ) = ( ( _i ^ k ) S y ) )
16 11 12 15 oveq123d 
 |-  ( u = U -> ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) = ( x G ( ( _i ^ k ) S y ) ) )
17 9 16 fveq12d 
 |-  ( u = U -> ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) = ( N ` ( x G ( ( _i ^ k ) S y ) ) ) )
18 17 oveq1d 
 |-  ( u = U -> ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) = ( ( N ` ( x G ( ( _i ^ k ) S y ) ) ) ^ 2 ) )
19 18 oveq2d 
 |-  ( u = U -> ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) ) = ( ( _i ^ k ) x. ( ( N ` ( x G ( ( _i ^ k ) S y ) ) ) ^ 2 ) ) )
20 19 sumeq2sdv 
 |-  ( u = U -> sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) ) = sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( x G ( ( _i ^ k ) S y ) ) ) ^ 2 ) ) )
21 20 oveq1d 
 |-  ( u = U -> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) ) / 4 ) = ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( x G ( ( _i ^ k ) S y ) ) ) ^ 2 ) ) / 4 ) )
22 7 7 21 mpoeq123dv 
 |-  ( u = U -> ( x e. ( BaseSet ` u ) , y e. ( BaseSet ` u ) |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) ) / 4 ) ) = ( x e. X , y e. X |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( x G ( ( _i ^ k ) S y ) ) ) ^ 2 ) ) / 4 ) ) )
23 df-dip 
 |-  .iOLD = ( u e. NrmCVec |-> ( x e. ( BaseSet ` u ) , y e. ( BaseSet ` u ) |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) ) / 4 ) ) )
24 1 fvexi 
 |-  X e. _V
25 24 24 mpoex 
 |-  ( x e. X , y e. X |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( x G ( ( _i ^ k ) S y ) ) ) ^ 2 ) ) / 4 ) ) e. _V
26 22 23 25 fvmpt 
 |-  ( U e. NrmCVec -> ( .iOLD ` U ) = ( x e. X , y e. X |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( x G ( ( _i ^ k ) S y ) ) ) ^ 2 ) ) / 4 ) ) )
27 5 26 syl5eq 
 |-  ( U e. NrmCVec -> P = ( x e. X , y e. X |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( x G ( ( _i ^ k ) S y ) ) ) ^ 2 ) ) / 4 ) ) )