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

Definition df-ph 21353
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  g, the scalar product is  s, and the norm is  n. 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  |-  CPreHil OLD  =  ( NrmCVec  i^i  { <. <. g ,  s >. ,  n >.  |  A. x  e. 
ran  g A. y  e.  ran  g ( ( ( n `  (
x g y ) ) ^ 2 )  +  ( ( n `
 ( x g ( -u 1 s y ) ) ) ^ 2 ) )  =  ( 2  x.  ( ( ( n `
 x ) ^
2 )  +  ( ( n `  y
) ^ 2 ) ) ) } )
Distinct variable group:    g, n, s, x, y

Detailed syntax breakdown of Definition df-ph
StepHypRef Expression
1 ccphlo 21352 . 2  class  CPreHil OLD
2 cnv 21102 . . 3  class  NrmCVec
3 vx . . . . . . . . . . . 12  set  x
43cv 1618 . . . . . . . . . . 11  class  x
5 vy . . . . . . . . . . . 12  set  y
65cv 1618 . . . . . . . . . . 11  class  y
7 vg . . . . . . . . . . . 12  set  g
87cv 1618 . . . . . . . . . . 11  class  g
94, 6, 8co 5793 . . . . . . . . . 10  class  ( x g y )
10 vn . . . . . . . . . . 11  set  n
1110cv 1618 . . . . . . . . . 10  class  n
129, 11cfv 5195 . . . . . . . . 9  class  ( n `
 ( x g y ) )
13 c2 9764 . . . . . . . . 9  class  2
14 cexp 11072 . . . . . . . . 9  class  ^
1512, 13, 14co 5793 . . . . . . . 8  class  ( ( n `  ( x g y ) ) ^ 2 )
16 c1 8707 . . . . . . . . . . . . 13  class  1
1716cneg 9007 . . . . . . . . . . . 12  class  -u 1
18 vs . . . . . . . . . . . . 13  set  s
1918cv 1618 . . . . . . . . . . . 12  class  s
2017, 6, 19co 5793 . . . . . . . . . . 11  class  ( -u
1 s y )
214, 20, 8co 5793 . . . . . . . . . 10  class  ( x g ( -u 1
s y ) )
2221, 11cfv 5195 . . . . . . . . 9  class  ( n `
 ( x g ( -u 1 s y ) ) )
2322, 13, 14co 5793 . . . . . . . 8  class  ( ( n `  ( x g ( -u 1
s y ) ) ) ^ 2 )
24 caddc 8709 . . . . . . . 8  class  +
2515, 23, 24co 5793 . . . . . . 7  class  ( ( ( n `  (
x g y ) ) ^ 2 )  +  ( ( n `
 ( x g ( -u 1 s y ) ) ) ^ 2 ) )
264, 11cfv 5195 . . . . . . . . . 10  class  ( n `
 x )
2726, 13, 14co 5793 . . . . . . . . 9  class  ( ( n `  x ) ^ 2 )
286, 11cfv 5195 . . . . . . . . . 10  class  ( n `
 y )
2928, 13, 14co 5793 . . . . . . . . 9  class  ( ( n `  y ) ^ 2 )
3027, 29, 24co 5793 . . . . . . . 8  class  ( ( ( n `  x
) ^ 2 )  +  ( ( n `
 y ) ^
2 ) )
31 cmul 8711 . . . . . . . 8  class  x.
3213, 30, 31co 5793 . . . . . . 7  class  ( 2  x.  ( ( ( n `  x ) ^ 2 )  +  ( ( n `  y ) ^ 2 ) ) )
3325, 32wceq 1619 . . . . . 6  wff  ( ( ( n `  (
x g y ) ) ^ 2 )  +  ( ( n `
 ( x g ( -u 1 s y ) ) ) ^ 2 ) )  =  ( 2  x.  ( ( ( n `
 x ) ^
2 )  +  ( ( n `  y
) ^ 2 ) ) )
348crn 4663 . . . . . 6  class  ran  g
3533, 5, 34wral 2518 . . . . 5  wff  A. y  e.  ran  g ( ( ( n `  (
x g y ) ) ^ 2 )  +  ( ( n `
 ( x g ( -u 1 s y ) ) ) ^ 2 ) )  =  ( 2  x.  ( ( ( n `
 x ) ^
2 )  +  ( ( n `  y
) ^ 2 ) ) )
3635, 3, 34wral 2518 . . . 4  wff  A. x  e.  ran  g A. y  e.  ran  g ( ( ( n `  (
x g y ) ) ^ 2 )  +  ( ( n `
 ( x g ( -u 1 s y ) ) ) ^ 2 ) )  =  ( 2  x.  ( ( ( n `
 x ) ^
2 )  +  ( ( n `  y
) ^ 2 ) ) )
3736, 7, 18, 10coprab 5794 . . 3  class  { <. <.
g ,  s >. ,  n >.  |  A. x  e.  ran  g A. y  e.  ran  g ( ( ( n `  ( x g y ) ) ^ 2 )  +  ( ( n `  ( x g ( -u 1
s y ) ) ) ^ 2 ) )  =  ( 2  x.  ( ( ( n `  x ) ^ 2 )  +  ( ( n `  y ) ^ 2 ) ) ) }
382, 37cin 3126 . 2  class  ( NrmCVec  i^i 
{ <. <. g ,  s
>. ,  n >.  | 
A. x  e.  ran  g A. y  e.  ran  g ( ( ( n `  ( x g y ) ) ^ 2 )  +  ( ( n `  ( x g (
-u 1 s y ) ) ) ^
2 ) )  =  ( 2  x.  (
( ( n `  x ) ^ 2 )  +  ( ( n `  y ) ^ 2 ) ) ) } )
391, 38wceq 1619 1  wff  CPreHil OLD  =  ( NrmCVec  i^i  { <. <. g ,  s >. ,  n >.  |  A. x  e. 
ran  g A. y  e.  ran  g ( ( ( n `  (
x g y ) ) ^ 2 )  +  ( ( n `
 ( x g ( -u 1 s y ) ) ) ^ 2 ) )  =  ( 2  x.  ( ( ( n `
 x ) ^
2 )  +  ( ( n `  y
) ^ 2 ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  phnv  21354  isphg  21357
  Copyright terms: Public domain W3C validator