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

Definition df-ph 22319
 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 22318 . 2
2 cnv 22068 . . 3
3 vx . . . . . . . . . . . 12
43cv 1652 . . . . . . . . . . 11
5 vy . . . . . . . . . . . 12
65cv 1652 . . . . . . . . . . 11
7 vg . . . . . . . . . . . 12
87cv 1652 . . . . . . . . . . 11
94, 6, 8co 6084 . . . . . . . . . 10
10 vn . . . . . . . . . . 11
1110cv 1652 . . . . . . . . . 10
129, 11cfv 5457 . . . . . . . . 9
13 c2 10054 . . . . . . . . 9
14 cexp 11387 . . . . . . . . 9
1512, 13, 14co 6084 . . . . . . . 8
16 c1 8996 . . . . . . . . . . . . 13
1716cneg 9297 . . . . . . . . . . . 12
18 vs . . . . . . . . . . . . 13
1918cv 1652 . . . . . . . . . . . 12
2017, 6, 19co 6084 . . . . . . . . . . 11
214, 20, 8co 6084 . . . . . . . . . 10
2221, 11cfv 5457 . . . . . . . . 9
2322, 13, 14co 6084 . . . . . . . 8
24 caddc 8998 . . . . . . . 8
2515, 23, 24co 6084 . . . . . . 7
264, 11cfv 5457 . . . . . . . . . 10
2726, 13, 14co 6084 . . . . . . . . 9
286, 11cfv 5457 . . . . . . . . . 10
2928, 13, 14co 6084 . . . . . . . . 9
3027, 29, 24co 6084 . . . . . . . 8
31 cmul 9000 . . . . . . . 8
3213, 30, 31co 6084 . . . . . . 7
3325, 32wceq 1653 . . . . . 6
348crn 4882 . . . . . 6
3533, 5, 34wral 2707 . . . . 5
3635, 3, 34wral 2707 . . . 4
3736, 7, 18, 10coprab 6085 . . 3
382, 37cin 3321 . 2
391, 38wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  phnv  22320  isphg  22323
 Copyright terms: Public domain W3C validator