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

Definition df-dip 21267
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  |-  .i OLD  =  ( 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
) ( .s OLD `  u ) y ) ) ) ^ 2 ) )  /  4
) ) )
Distinct variable group:    u, k, x, y

Detailed syntax breakdown of Definition df-dip
StepHypRef Expression
1 cdip 21266 . 2  class  .i OLD
2 vu . . 3  set  u
3 cnv 21133 . . 3  class  NrmCVec
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1623 . . . . 5  class  u
7 cba 21135 . . . . 5  class  BaseSet
86, 7cfv 5222 . . . 4  class  ( BaseSet `  u )
9 c1 8734 . . . . . . 7  class  1
10 c4 9793 . . . . . . 7  class  4
11 cfz 10777 . . . . . . 7  class  ...
129, 10, 11co 5820 . . . . . 6  class  ( 1 ... 4 )
13 ci 8735 . . . . . . . 8  class  _i
14 vk . . . . . . . . 9  set  k
1514cv 1623 . . . . . . . 8  class  k
16 cexp 11099 . . . . . . . 8  class  ^
1713, 15, 16co 5820 . . . . . . 7  class  ( _i
^ k )
184cv 1623 . . . . . . . . . 10  class  x
195cv 1623 . . . . . . . . . . 11  class  y
20 cns 21136 . . . . . . . . . . . 12  class  .s OLD
216, 20cfv 5222 . . . . . . . . . . 11  class  ( .s
OLD `  u )
2217, 19, 21co 5820 . . . . . . . . . 10  class  ( ( _i ^ k ) ( .s OLD `  u
) y )
23 cpv 21134 . . . . . . . . . . 11  class  +v
246, 23cfv 5222 . . . . . . . . . 10  class  ( +v
`  u )
2518, 22, 24co 5820 . . . . . . . . 9  class  ( x ( +v `  u
) ( ( _i
^ k ) ( .s OLD `  u
) y ) )
26 cnmcv 21139 . . . . . . . . . 10  class  normCV
276, 26cfv 5222 . . . . . . . . 9  class  ( normCV `  u )
2825, 27cfv 5222 . . . . . . . 8  class  ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) )
29 c2 9791 . . . . . . . 8  class  2
3028, 29, 16co 5820 . . . . . . 7  class  ( ( ( normCV `  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) ) ^ 2 )
31 cmul 8738 . . . . . . 7  class  x.
3217, 30, 31co 5820 . . . . . 6  class  ( ( _i ^ k )  x.  ( ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) ) ^ 2 ) )
3312, 32, 14csu 12153 . . . . 5  class  sum_ k  e.  ( 1 ... 4
) ( ( _i
^ k )  x.  ( ( ( normCV `  u ) `  (
x ( +v `  u ) ( ( _i ^ k ) ( .s OLD `  u
) y ) ) ) ^ 2 ) )
34 cdiv 9419 . . . . 5  class  /
3533, 10, 34co 5820 . . . 4  class  ( sum_ k  e.  ( 1 ... 4 ) ( ( _i ^ k
)  x.  ( ( ( normCV `  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) ) ^ 2 ) )  /  4
)
364, 5, 8, 8, 35cmpt2 5822 . . 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 ) ( .s OLD `  u
) y ) ) ) ^ 2 ) )  /  4 ) )
372, 3, 36cmpt 4079 . 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 ) ( .s OLD `  u
) y ) ) ) ^ 2 ) )  /  4 ) ) )
381, 37wceq 1624 1  wff  .i OLD  =  ( 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
) ( .s OLD `  u ) y ) ) ) ^ 2 ) )  /  4
) ) )
Colors of variables: wff set class
This definition is referenced by:  dipfval  21268
  Copyright terms: Public domain W3C validator