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

Definition df-ph 22302
 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 22301 . 2
2 cnv 22051 . . 3
3 vx . . . . . . . . . . . 12
43cv 1651 . . . . . . . . . . 11
5 vy . . . . . . . . . . . 12
65cv 1651 . . . . . . . . . . 11
7 vg . . . . . . . . . . . 12
87cv 1651 . . . . . . . . . . 11
94, 6, 8co 6072 . . . . . . . . . 10
10 vn . . . . . . . . . . 11
1110cv 1651 . . . . . . . . . 10
129, 11cfv 5445 . . . . . . . . 9
13 c2 10038 . . . . . . . . 9
14 cexp 11370 . . . . . . . . 9
1512, 13, 14co 6072 . . . . . . . 8
16 c1 8980 . . . . . . . . . . . . 13
1716cneg 9281 . . . . . . . . . . . 12
18 vs . . . . . . . . . . . . 13
1918cv 1651 . . . . . . . . . . . 12
2017, 6, 19co 6072 . . . . . . . . . . 11
214, 20, 8co 6072 . . . . . . . . . 10
2221, 11cfv 5445 . . . . . . . . 9
2322, 13, 14co 6072 . . . . . . . 8
24 caddc 8982 . . . . . . . 8
2515, 23, 24co 6072 . . . . . . 7
264, 11cfv 5445 . . . . . . . . . 10
2726, 13, 14co 6072 . . . . . . . . 9
286, 11cfv 5445 . . . . . . . . . 10
2928, 13, 14co 6072 . . . . . . . . 9
3027, 29, 24co 6072 . . . . . . . 8
31 cmul 8984 . . . . . . . 8
3213, 30, 31co 6072 . . . . . . 7
3325, 32wceq 1652 . . . . . 6
348crn 4870 . . . . . 6
3533, 5, 34wral 2697 . . . . 5
3635, 3, 34wral 2697 . . . 4
3736, 7, 18, 10coprab 6073 . . 3
382, 37cin 3311 . 2
391, 38wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  phnv  22303  isphg  22306
 Copyright terms: Public domain W3C validator