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

Definition df-dip 21274
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 21273 . 2  class  .i OLD
2 vu . . 3  set  u
3 cnv 21140 . . 3  class  NrmCVec
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1622 . . . . 5  class  u
7 cba 21142 . . . . 5  class  BaseSet
86, 7cfv 5255 . . . 4  class  ( BaseSet `  u )
9 c1 8738 . . . . . . 7  class  1
10 c4 9797 . . . . . . 7  class  4
11 cfz 10782 . . . . . . 7  class  ...
129, 10, 11co 5858 . . . . . 6  class  ( 1 ... 4 )
13 ci 8739 . . . . . . . 8  class  _i
14 vk . . . . . . . . 9  set  k
1514cv 1622 . . . . . . . 8  class  k
16 cexp 11104 . . . . . . . 8  class  ^
1713, 15, 16co 5858 . . . . . . 7  class  ( _i
^ k )
184cv 1622 . . . . . . . . . 10  class  x
195cv 1622 . . . . . . . . . . 11  class  y
20 cns 21143 . . . . . . . . . . . 12  class  .s OLD
216, 20cfv 5255 . . . . . . . . . . 11  class  ( .s
OLD `  u )
2217, 19, 21co 5858 . . . . . . . . . 10  class  ( ( _i ^ k ) ( .s OLD `  u
) y )
23 cpv 21141 . . . . . . . . . . 11  class  +v
246, 23cfv 5255 . . . . . . . . . 10  class  ( +v
`  u )
2518, 22, 24co 5858 . . . . . . . . 9  class  ( x ( +v `  u
) ( ( _i
^ k ) ( .s OLD `  u
) y ) )
26 cnmcv 21146 . . . . . . . . . 10  class  normCV
276, 26cfv 5255 . . . . . . . . 9  class  ( normCV `  u )
2825, 27cfv 5255 . . . . . . . 8  class  ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) )
29 c2 9795 . . . . . . . 8  class  2
3028, 29, 16co 5858 . . . . . . 7  class  ( ( ( normCV `  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) ) ^ 2 )
31 cmul 8742 . . . . . . 7  class  x.
3217, 30, 31co 5858 . . . . . 6  class  ( ( _i ^ k )  x.  ( ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) ) ^ 2 ) )
3312, 32, 14csu 12158 . . . . 5  class  sum_ k  e.  ( 1 ... 4
) ( ( _i
^ k )  x.  ( ( ( normCV `  u ) `  (
x ( +v `  u ) ( ( _i ^ k ) ( .s OLD `  u
) y ) ) ) ^ 2 ) )
34 cdiv 9423 . . . . 5  class  /
3533, 10, 34co 5858 . . . 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 5860 . . 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 4077 . 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 1623 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  21275
  Copyright terms: Public domain W3C validator