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

Definition df-dip 22150
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 22149 . 2  class  .i OLD
2 vu . . 3  set  u
3 cnv 22016 . . 3  class  NrmCVec
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1648 . . . . 5  class  u
7 cba 22018 . . . . 5  class  BaseSet
86, 7cfv 5413 . . . 4  class  ( BaseSet `  u )
9 c1 8947 . . . . . . 7  class  1
10 c4 10007 . . . . . . 7  class  4
11 cfz 10999 . . . . . . 7  class  ...
129, 10, 11co 6040 . . . . . 6  class  ( 1 ... 4 )
13 ci 8948 . . . . . . . 8  class  _i
14 vk . . . . . . . . 9  set  k
1514cv 1648 . . . . . . . 8  class  k
16 cexp 11337 . . . . . . . 8  class  ^
1713, 15, 16co 6040 . . . . . . 7  class  ( _i
^ k )
184cv 1648 . . . . . . . . . 10  class  x
195cv 1648 . . . . . . . . . . 11  class  y
20 cns 22019 . . . . . . . . . . . 12  class  .s OLD
216, 20cfv 5413 . . . . . . . . . . 11  class  ( .s
OLD `  u )
2217, 19, 21co 6040 . . . . . . . . . 10  class  ( ( _i ^ k ) ( .s OLD `  u
) y )
23 cpv 22017 . . . . . . . . . . 11  class  +v
246, 23cfv 5413 . . . . . . . . . 10  class  ( +v
`  u )
2518, 22, 24co 6040 . . . . . . . . 9  class  ( x ( +v `  u
) ( ( _i
^ k ) ( .s OLD `  u
) y ) )
26 cnmcv 22022 . . . . . . . . . 10  class  normCV
276, 26cfv 5413 . . . . . . . . 9  class  ( normCV `  u )
2825, 27cfv 5413 . . . . . . . 8  class  ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) )
29 c2 10005 . . . . . . . 8  class  2
3028, 29, 16co 6040 . . . . . . 7  class  ( ( ( normCV `  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) ) ^ 2 )
31 cmul 8951 . . . . . . 7  class  x.
3217, 30, 31co 6040 . . . . . 6  class  ( ( _i ^ k )  x.  ( ( (
normCV
`  u ) `  ( x ( +v
`  u ) ( ( _i ^ k
) ( .s OLD `  u ) y ) ) ) ^ 2 ) )
3312, 32, 14csu 12434 . . . . 5  class  sum_ k  e.  ( 1 ... 4
) ( ( _i
^ k )  x.  ( ( ( normCV `  u ) `  (
x ( +v `  u ) ( ( _i ^ k ) ( .s OLD `  u
) y ) ) ) ^ 2 ) )
34 cdiv 9633 . . . . 5  class  /
3533, 10, 34co 6040 . . . 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 6042 . . 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 4226 . 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 1649 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  22151
  Copyright terms: Public domain W3C validator