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

Definition df-dip 22189
 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 , the scalar product is , and the norm is . (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.)
Assertion
Ref Expression
df-dip
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-dip
StepHypRef Expression
1 cdip 22188 . 2
2 vu . . 3
3 cnv 22055 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1651 . . . . 5
7 cba 22057 . . . . 5
86, 7cfv 5446 . . . 4
9 c1 8983 . . . . . . 7
10 c4 10043 . . . . . . 7
11 cfz 11035 . . . . . . 7
129, 10, 11co 6073 . . . . . 6
13 ci 8984 . . . . . . . 8
14 vk . . . . . . . . 9
1514cv 1651 . . . . . . . 8
16 cexp 11374 . . . . . . . 8
1713, 15, 16co 6073 . . . . . . 7
184cv 1651 . . . . . . . . . 10
195cv 1651 . . . . . . . . . . 11
20 cns 22058 . . . . . . . . . . . 12
216, 20cfv 5446 . . . . . . . . . . 11
2217, 19, 21co 6073 . . . . . . . . . 10
23 cpv 22056 . . . . . . . . . . 11
246, 23cfv 5446 . . . . . . . . . 10
2518, 22, 24co 6073 . . . . . . . . 9
26 cnmcv 22061 . . . . . . . . . 10
276, 26cfv 5446 . . . . . . . . 9
2825, 27cfv 5446 . . . . . . . 8
29 c2 10041 . . . . . . . 8
3028, 29, 16co 6073 . . . . . . 7
31 cmul 8987 . . . . . . 7
3217, 30, 31co 6073 . . . . . 6
3312, 32, 14csu 12471 . . . . 5
34 cdiv 9669 . . . . 5
3533, 10, 34co 6073 . . . 4
364, 5, 8, 8, 35cmpt2 6075 . . 3
372, 3, 36cmpt 4258 . 2
381, 37wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  dipfval  22190
 Copyright terms: Public domain W3C validator