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

Definition df-dip 21199
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 21198 . 2  class  .i OLD
2 vu . . 3  set  u
3 cnv 21065 . . 3  class  NrmCVec
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1618 . . . . 5  class  u
7 cba 21067 . . . . 5  class  BaseSet
86, 7cfv 4638 . . . 4  class  ( BaseSet `  u )
9 c1 8671 . . . . . . 7  class  1
10 c4 9730 . . . . . . 7  class  4
11 cfz 10713 . . . . . . 7  class  ...
129, 10, 11co 5757 . . . . . 6  class  ( 1 ... 4 )
13 ci 8672 . . . . . . . 8  class  _i
14 vk . . . . . . . . 9  set  k
1514cv 1618 . . . . . . . 8  class  k
16 cexp 11035 . . . . . . . 8  class  ^
1713, 15, 16co 5757 . . . . . . 7  class  ( _i
^ k )
184cv 1618 . . . . . . . . . 10  class  x
195cv 1618 . . . . . . . . . . 11  class  y
20 cns 21068 . . . . . . . . . . . 12  class  .s OLD
216, 20cfv 4638 . . . . . . . . . . 11  class  ( .s
OLD `  u )
2217, 19, 21co 5757 . . . . . . . . . 10  class  ( ( _i ^ k ) ( .s OLD `  u
) y )
23 cpv 21066 . . . . . . . . . . 11  class  +v
246, 23cfv 4638 . . . . . . . . . 10  class  ( +v
`  u )
2518, 22, 24co 5757 . . . . . . . . 9  class  ( x ( +v `  u
) ( ( _i
^ k ) ( .s OLD `  u
) y ) )
26 cnmcv 21071 . . . . . . . . . 10  class  normCV
276, 26cfv 4638 . . . . . . . . 9  class  ( normCV `  u )
2825, 27cfv 4638 . . . . . . . 8  class  ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) )
29 c2 9728 . . . . . . . 8  class  2
3028, 29, 16co 5757 . . . . . . 7  class  ( ( ( normCV `  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) ) ^ 2 )
31 cmul 8675 . . . . . . 7  class  x.
3217, 30, 31co 5757 . . . . . 6  class  ( ( _i ^ k )  x.  ( ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) ) ^ 2 ) )
3312, 32, 14csu 12088 . . . . 5  class  sum_ k  e.  ( 1 ... 4
) ( ( _i
^ k )  x.  ( ( ( normCV `  u ) `  (
x ( +v `  u ) ( ( _i ^ k ) ( .s OLD `  u
) y ) ) ) ^ 2 ) )
34 cdiv 9356 . . . . 5  class  /
3533, 10, 34co 5757 . . . 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 5759 . . 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 4017 . 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 1619 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  21200
  Copyright terms: Public domain W3C validator