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

Definition df-dip 22233
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 22232 . 2
2 vu . . 3
3 cnv 22099 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1653 . . . . 5
7 cba 22101 . . . . 5
86, 7cfv 5505 . . . 4
9 c1 9046 . . . . . . 7
10 c4 10106 . . . . . . 7
11 cfz 11098 . . . . . . 7
129, 10, 11co 6133 . . . . . 6
13 ci 9047 . . . . . . . 8
14 vk . . . . . . . . 9
1514cv 1653 . . . . . . . 8
16 cexp 11437 . . . . . . . 8
1713, 15, 16co 6133 . . . . . . 7
184cv 1653 . . . . . . . . . 10
195cv 1653 . . . . . . . . . . 11
20 cns 22102 . . . . . . . . . . . 12
216, 20cfv 5505 . . . . . . . . . . 11
2217, 19, 21co 6133 . . . . . . . . . 10
23 cpv 22100 . . . . . . . . . . 11
246, 23cfv 5505 . . . . . . . . . 10
2518, 22, 24co 6133 . . . . . . . . 9
26 cnmcv 22105 . . . . . . . . . 10
276, 26cfv 5505 . . . . . . . . 9
2825, 27cfv 5505 . . . . . . . 8
29 c2 10104 . . . . . . . 8
3028, 29, 16co 6133 . . . . . . 7
31 cmul 9050 . . . . . . 7
3217, 30, 31co 6133 . . . . . 6
3312, 32, 14csu 12534 . . . . 5
34 cdiv 9732 . . . . 5
3533, 10, 34co 6133 . . . 4
364, 5, 8, 8, 35cmpt2 6135 . . 3
372, 3, 36cmpt 4305 . 2
381, 37wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  dipfval  22234
  Copyright terms: Public domain W3C validator