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

Definition df-dip 26386
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 26385 . 2  class  .iOLD
2 vu . . 3  setvar  u
3 cnv 26252 . . 3  class  NrmCVec
4 vx . . . 4  setvar  x
5 vy . . . 4  setvar  y
62cv 1454 . . . . 5  class  u
7 cba 26254 . . . . 5  class  BaseSet
86, 7cfv 5601 . . . 4  class  ( BaseSet `  u )
9 c1 9566 . . . . . . 7  class  1
10 c4 10689 . . . . . . 7  class  4
11 cfz 11813 . . . . . . 7  class  ...
129, 10, 11co 6315 . . . . . 6  class  ( 1 ... 4 )
13 ci 9567 . . . . . . . 8  class  _i
14 vk . . . . . . . . 9  setvar  k
1514cv 1454 . . . . . . . 8  class  k
16 cexp 12304 . . . . . . . 8  class  ^
1713, 15, 16co 6315 . . . . . . 7  class  ( _i
^ k )
184cv 1454 . . . . . . . . . 10  class  x
195cv 1454 . . . . . . . . . . 11  class  y
20 cns 26255 . . . . . . . . . . . 12  class  .sOLD
216, 20cfv 5601 . . . . . . . . . . 11  class  ( .sOLD `  u )
2217, 19, 21co 6315 . . . . . . . . . 10  class  ( ( _i ^ k ) ( .sOLD `  u ) y )
23 cpv 26253 . . . . . . . . . . 11  class  +v
246, 23cfv 5601 . . . . . . . . . 10  class  ( +v
`  u )
2518, 22, 24co 6315 . . . . . . . . 9  class  ( x ( +v `  u
) ( ( _i
^ k ) ( .sOLD `  u
) y ) )
26 cnmcv 26258 . . . . . . . . . 10  class  normCV
276, 26cfv 5601 . . . . . . . . 9  class  ( normCV `  u )
2825, 27cfv 5601 . . . . . . . 8  class  ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .sOLD `  u ) y ) ) )
29 c2 10687 . . . . . . . 8  class  2
3028, 29, 16co 6315 . . . . . . 7  class  ( ( ( normCV `  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .sOLD `  u ) y ) ) ) ^ 2 )
31 cmul 9570 . . . . . . 7  class  x.
3217, 30, 31co 6315 . . . . . 6  class  ( ( _i ^ k )  x.  ( ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .sOLD `  u ) y ) ) ) ^ 2 ) )
3312, 32, 14csu 13801 . . . . 5  class  sum_ k  e.  ( 1 ... 4
) ( ( _i
^ k )  x.  ( ( ( normCV `  u ) `  (
x ( +v `  u ) ( ( _i ^ k ) ( .sOLD `  u ) y ) ) ) ^ 2 ) )
34 cdiv 10297 . . . . 5  class  /
3533, 10, 34co 6315 . . . 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 6317 . . 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 4475 . 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 1455 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  26387
  Copyright terms: Public domain W3C validator