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

Definition df-dip 21104
 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 CV
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-dip
StepHypRef Expression
1 cdip 21103 . 2
2 vu . . 3
3 cnv 20970 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1618 . . . . 5
7 cba 20972 . . . . 5
86, 7cfv 4592 . . . 4
9 c1 8618 . . . . . . 7
10 c4 9677 . . . . . . 7
11 cfz 10660 . . . . . . 7
129, 10, 11co 5710 . . . . . 6
13 ci 8619 . . . . . . . 8
14 vk . . . . . . . . 9
1514cv 1618 . . . . . . . 8
16 cexp 10982 . . . . . . . 8
1713, 15, 16co 5710 . . . . . . 7
184cv 1618 . . . . . . . . . 10
195cv 1618 . . . . . . . . . . 11
20 cns 20973 . . . . . . . . . . . 12
216, 20cfv 4592 . . . . . . . . . . 11
2217, 19, 21co 5710 . . . . . . . . . 10
23 cpv 20971 . . . . . . . . . . 11
246, 23cfv 4592 . . . . . . . . . 10
2518, 22, 24co 5710 . . . . . . . . 9
26 cnmcv 20976 . . . . . . . . . 10 CV
276, 26cfv 4592 . . . . . . . . 9 CV
2825, 27cfv 4592 . . . . . . . 8 CV
29 c2 9675 . . . . . . . 8
3028, 29, 16co 5710 . . . . . . 7 CV
31 cmul 8622 . . . . . . 7
3217, 30, 31co 5710 . . . . . 6 CV
3312, 32, 14csu 12035 . . . . 5 CV
34 cdiv 9303 . . . . 5
3533, 10, 34co 5710 . . . 4 CV
364, 5, 8, 8, 35cmpt2 5712 . . 3 CV
372, 3, 36cmpt 3974 . 2 CV
381, 37wceq 1619 1 CV
 Colors of variables: wff set class This definition is referenced by:  dipfval  21105
 Copyright terms: Public domain W3C validator