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

Definition df-dip 22197
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 22196 . 2  class  .i OLD
2 vu . . 3  set  u
3 cnv 22063 . . 3  class  NrmCVec
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1651 . . . . 5  class  u
7 cba 22065 . . . . 5  class  BaseSet
86, 7cfv 5454 . . . 4  class  ( BaseSet `  u )
9 c1 8991 . . . . . . 7  class  1
10 c4 10051 . . . . . . 7  class  4
11 cfz 11043 . . . . . . 7  class  ...
129, 10, 11co 6081 . . . . . 6  class  ( 1 ... 4 )
13 ci 8992 . . . . . . . 8  class  _i
14 vk . . . . . . . . 9  set  k
1514cv 1651 . . . . . . . 8  class  k
16 cexp 11382 . . . . . . . 8  class  ^
1713, 15, 16co 6081 . . . . . . 7  class  ( _i
^ k )
184cv 1651 . . . . . . . . . 10  class  x
195cv 1651 . . . . . . . . . . 11  class  y
20 cns 22066 . . . . . . . . . . . 12  class  .s OLD
216, 20cfv 5454 . . . . . . . . . . 11  class  ( .s
OLD `  u )
2217, 19, 21co 6081 . . . . . . . . . 10  class  ( ( _i ^ k ) ( .s OLD `  u
) y )
23 cpv 22064 . . . . . . . . . . 11  class  +v
246, 23cfv 5454 . . . . . . . . . 10  class  ( +v
`  u )
2518, 22, 24co 6081 . . . . . . . . 9  class  ( x ( +v `  u
) ( ( _i
^ k ) ( .s OLD `  u
) y ) )
26 cnmcv 22069 . . . . . . . . . 10  class  normCV
276, 26cfv 5454 . . . . . . . . 9  class  ( normCV `  u )
2825, 27cfv 5454 . . . . . . . 8  class  ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) )
29 c2 10049 . . . . . . . 8  class  2
3028, 29, 16co 6081 . . . . . . 7  class  ( ( ( normCV `  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) ) ^ 2 )
31 cmul 8995 . . . . . . 7  class  x.
3217, 30, 31co 6081 . . . . . 6  class  ( ( _i ^ k )  x.  ( ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) ) ^ 2 ) )
3312, 32, 14csu 12479 . . . . 5  class  sum_ k  e.  ( 1 ... 4
) ( ( _i
^ k )  x.  ( ( ( normCV `  u ) `  (
x ( +v `  u ) ( ( _i ^ k ) ( .s OLD `  u
) y ) ) ) ^ 2 ) )
34 cdiv 9677 . . . . 5  class  /
3533, 10, 34co 6081 . . . 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 6083 . . 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 4266 . 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 1652 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  22198
  Copyright terms: Public domain W3C validator