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

Definition df-dip 25442
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 25441 . 2  class  .iOLD
2 vu . . 3  setvar  u
3 cnv 25308 . . 3  class  NrmCVec
4 vx . . . 4  setvar  x
5 vy . . . 4  setvar  y
62cv 1378 . . . . 5  class  u
7 cba 25310 . . . . 5  class  BaseSet
86, 7cfv 5594 . . . 4  class  ( BaseSet `  u )
9 c1 9505 . . . . . . 7  class  1
10 c4 10599 . . . . . . 7  class  4
11 cfz 11684 . . . . . . 7  class  ...
129, 10, 11co 6295 . . . . . 6  class  ( 1 ... 4 )
13 ci 9506 . . . . . . . 8  class  _i
14 vk . . . . . . . . 9  setvar  k
1514cv 1378 . . . . . . . 8  class  k
16 cexp 12146 . . . . . . . 8  class  ^
1713, 15, 16co 6295 . . . . . . 7  class  ( _i
^ k )
184cv 1378 . . . . . . . . . 10  class  x
195cv 1378 . . . . . . . . . . 11  class  y
20 cns 25311 . . . . . . . . . . . 12  class  .sOLD
216, 20cfv 5594 . . . . . . . . . . 11  class  ( .sOLD `  u )
2217, 19, 21co 6295 . . . . . . . . . 10  class  ( ( _i ^ k ) ( .sOLD `  u ) y )
23 cpv 25309 . . . . . . . . . . 11  class  +v
246, 23cfv 5594 . . . . . . . . . 10  class  ( +v
`  u )
2518, 22, 24co 6295 . . . . . . . . 9  class  ( x ( +v `  u
) ( ( _i
^ k ) ( .sOLD `  u
) y ) )
26 cnmcv 25314 . . . . . . . . . 10  class  normCV
276, 26cfv 5594 . . . . . . . . 9  class  ( normCV `  u )
2825, 27cfv 5594 . . . . . . . 8  class  ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .sOLD `  u ) y ) ) )
29 c2 10597 . . . . . . . 8  class  2
3028, 29, 16co 6295 . . . . . . 7  class  ( ( ( normCV `  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .sOLD `  u ) y ) ) ) ^ 2 )
31 cmul 9509 . . . . . . 7  class  x.
3217, 30, 31co 6295 . . . . . 6  class  ( ( _i ^ k )  x.  ( ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .sOLD `  u ) y ) ) ) ^ 2 ) )
3312, 32, 14csu 13487 . . . . 5  class  sum_ k  e.  ( 1 ... 4
) ( ( _i
^ k )  x.  ( ( ( normCV `  u ) `  (
x ( +v `  u ) ( ( _i ^ k ) ( .sOLD `  u ) y ) ) ) ^ 2 ) )
34 cdiv 10218 . . . . 5  class  /
3533, 10, 34co 6295 . . . 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 6297 . . 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 4511 . 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 1379 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  25443
  Copyright terms: Public domain W3C validator