Metamath Proof Explorer

Definition df-dip

Description: Define a function that maps a normed complex vector space to its inner product operation in case its norm satisfies the parallelogram identity (otherwise the operation is still defined, but not meaningful). Based on Exercise 4(a) of ReedSimon p. 63 and Theorem 6.44 of Ponnusamy p. 361. Vector addition is ( 1stw ) , the scalar product is ( 2ndw ) , and the norm is n . (Contributed by NM, 10-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion 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 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdip 
 |-  .iOLD
1 vu 
 |-  u
2 cnv 
 |-  NrmCVec
3 vx 
 |-  x
4 cba 
 |-  BaseSet
5 1 cv 
 |-  u
6 5 4 cfv 
 |-  ( BaseSet ` u )
7 vy 
 |-  y
8 vk 
 |-  k
9 c1 
 |-  1
10 cfz 
 |-  ...
11 c4 
 |-  4
12 9 11 10 co 
 |-  ( 1 ... 4 )
13 ci 
 |-  _i
14 cexp 
 |-  ^
15 8 cv 
 |-  k
16 13 15 14 co 
 |-  ( _i ^ k )
17 cmul 
 |-  x.
18 cnmcv 
 |-  normCV
19 5 18 cfv 
 |-  ( normCV ` u )
20 3 cv 
 |-  x
21 cpv 
 |-  +v
22 5 21 cfv 
 |-  ( +v ` u )
23 cns 
 |-  .sOLD
24 5 23 cfv 
 |-  ( .sOLD ` u )
25 7 cv 
 |-  y
26 16 25 24 co 
 |-  ( ( _i ^ k ) ( .sOLD ` u ) y )
27 20 26 22 co 
 |-  ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) )
28 27 19 cfv 
 |-  ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) )
29 c2 
 |-  2
30 28 29 14 co 
 |-  ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 )
31 16 30 17 co 
 |-  ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) )
32 12 31 8 csu 
 |-  sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) )
33 cdiv 
 |-  /
34 32 11 33 co 
 |-  ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) ) / 4 )
35 3 7 6 6 34 cmpo 
 |-  ( 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 ) )
36 1 2 35 cmpt 
 |-  ( 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 ) ) )
37 0 36 wceq 
 |-  .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 ) ) )