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

Definition df-ph 21221
 Description: Define the class of all complex inner product spaces. An inner product space is a normed vector space whose norm satisfies the parallelogram law (a property that induces an inner product). Based on Exercise 4(b) of [ReedSimon] p. 63. The vector operation is , the scalar product is , and the norm is . An inner product space is also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.)
Assertion
Ref Expression
df-ph
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-ph
StepHypRef Expression
1 ccphlo 21220 . 2
2 cnv 20970 . . 3
3 vx . . . . . . . . . . . 12
43cv 1618 . . . . . . . . . . 11
5 vy . . . . . . . . . . . 12
65cv 1618 . . . . . . . . . . 11
7 vg . . . . . . . . . . . 12
87cv 1618 . . . . . . . . . . 11
94, 6, 8co 5710 . . . . . . . . . 10
10 vn . . . . . . . . . . 11
1110cv 1618 . . . . . . . . . 10
129, 11cfv 4592 . . . . . . . . 9
13 c2 9675 . . . . . . . . 9
14 cexp 10982 . . . . . . . . 9
1512, 13, 14co 5710 . . . . . . . 8
16 c1 8618 . . . . . . . . . . . . 13
1716cneg 8918 . . . . . . . . . . . 12
18 vs . . . . . . . . . . . . 13
1918cv 1618 . . . . . . . . . . . 12
2017, 6, 19co 5710 . . . . . . . . . . 11
214, 20, 8co 5710 . . . . . . . . . 10
2221, 11cfv 4592 . . . . . . . . 9
2322, 13, 14co 5710 . . . . . . . 8
24 caddc 8620 . . . . . . . 8
2515, 23, 24co 5710 . . . . . . 7
264, 11cfv 4592 . . . . . . . . . 10
2726, 13, 14co 5710 . . . . . . . . 9
286, 11cfv 4592 . . . . . . . . . 10
2928, 13, 14co 5710 . . . . . . . . 9
3027, 29, 24co 5710 . . . . . . . 8
31 cmul 8622 . . . . . . . 8
3213, 30, 31co 5710 . . . . . . 7
3325, 32wceq 1619 . . . . . 6
348crn 4581 . . . . . 6
3533, 5, 34wral 2509 . . . . 5
3635, 3, 34wral 2509 . . . 4
3736, 7, 18, 10copab2 5711 . . 3
382, 37cin 3077 . 2
391, 38wceq 1619 1
 Colors of variables: wff set class This definition is referenced by:  phnv  21222  isphg  21225
 Copyright terms: Public domain W3C validator