MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dip Structured version   Unicode version

Definition df-dip 25728
Description: Define a function that maps a complex normed 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  ( 1st `  w
), the scalar product is  ( 2nd `  w
), and the norm is  n. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.)
Assertion
Ref Expression
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
) ) )
Distinct variable group:    u, k, x, y

Detailed syntax breakdown of Definition df-dip
StepHypRef Expression
1 cdip 25727 . 2  class  .iOLD
2 vu . . 3  setvar  u
3 cnv 25594 . . 3  class  NrmCVec
4 vx . . . 4  setvar  x
5 vy . . . 4  setvar  y
62cv 1398 . . . . 5  class  u
7 cba 25596 . . . . 5  class  BaseSet
86, 7cfv 5496 . . . 4  class  ( BaseSet `  u )
9 c1 9404 . . . . . . 7  class  1
10 c4 10504 . . . . . . 7  class  4
11 cfz 11593 . . . . . . 7  class  ...
129, 10, 11co 6196 . . . . . 6  class  ( 1 ... 4 )
13 ci 9405 . . . . . . . 8  class  _i
14 vk . . . . . . . . 9  setvar  k
1514cv 1398 . . . . . . . 8  class  k
16 cexp 12069 . . . . . . . 8  class  ^
1713, 15, 16co 6196 . . . . . . 7  class  ( _i
^ k )
184cv 1398 . . . . . . . . . 10  class  x
195cv 1398 . . . . . . . . . . 11  class  y
20 cns 25597 . . . . . . . . . . . 12  class  .sOLD
216, 20cfv 5496 . . . . . . . . . . 11  class  ( .sOLD `  u )
2217, 19, 21co 6196 . . . . . . . . . 10  class  ( ( _i ^ k ) ( .sOLD `  u ) y )
23 cpv 25595 . . . . . . . . . . 11  class  +v
246, 23cfv 5496 . . . . . . . . . 10  class  ( +v
`  u )
2518, 22, 24co 6196 . . . . . . . . 9  class  ( x ( +v `  u
) ( ( _i
^ k ) ( .sOLD `  u
) y ) )
26 cnmcv 25600 . . . . . . . . . 10  class  normCV
276, 26cfv 5496 . . . . . . . . 9  class  ( normCV `  u )
2825, 27cfv 5496 . . . . . . . 8  class  ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .sOLD `  u ) y ) ) )
29 c2 10502 . . . . . . . 8  class  2
3028, 29, 16co 6196 . . . . . . 7  class  ( ( ( normCV `  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .sOLD `  u ) y ) ) ) ^ 2 )
31 cmul 9408 . . . . . . 7  class  x.
3217, 30, 31co 6196 . . . . . 6  class  ( ( _i ^ k )  x.  ( ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .sOLD `  u ) y ) ) ) ^ 2 ) )
3312, 32, 14csu 13510 . . . . 5  class  sum_ k  e.  ( 1 ... 4
) ( ( _i
^ k )  x.  ( ( ( normCV `  u ) `  (
x ( +v `  u ) ( ( _i ^ k ) ( .sOLD `  u ) y ) ) ) ^ 2 ) )
34 cdiv 10123 . . . . 5  class  /
3533, 10, 34co 6196 . . . 4  class  ( sum_ k  e.  ( 1 ... 4 ) ( ( _i ^ k
)  x.  ( ( ( normCV `  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .sOLD `  u ) y ) ) ) ^ 2 ) )  /  4
)
364, 5, 8, 8, 35cmpt2 6198 . . 3  class  ( 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 ) )
372, 3, 36cmpt 4425 . 2  class  ( 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 ) ) )
381, 37wceq 1399 1  wff  .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
) ) )
Colors of variables: wff setvar class
This definition is referenced by:  dipfval  25729
  Copyright terms: Public domain W3C validator