Metamath Proof Explorer

Definition df-ph

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.)

Ref Expression
Assertion df-ph 
|- CPreHilOLD = ( 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 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccphlo 
 |-  CPreHilOLD
1 cnv 
 |-  NrmCVec
2 vg 
 |-  g
3 vs 
 |-  s
4 vn 
 |-  n
5 vx 
 |-  x
6 2 cv 
 |-  g
7 6 crn 
 |-  ran g
8 vy 
 |-  y
9 4 cv 
 |-  n
10 5 cv 
 |-  x
11 8 cv 
 |-  y
12 10 11 6 co 
 |-  ( x g y )
13 12 9 cfv 
 |-  ( n ` ( x g y ) )
14 cexp 
 |-  ^
15 c2 
 |-  2
16 13 15 14 co 
 |-  ( ( n ` ( x g y ) ) ^ 2 )
17 caddc 
 |-  +
18 c1 
 |-  1
19 18 cneg 
 |-  -u 1
20 3 cv 
 |-  s
21 19 11 20 co 
 |-  ( -u 1 s y )
22 10 21 6 co 
 |-  ( x g ( -u 1 s y ) )
23 22 9 cfv 
 |-  ( n ` ( x g ( -u 1 s y ) ) )
24 23 15 14 co 
 |-  ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 )
25 16 24 17 co 
 |-  ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) )
26 cmul 
 |-  x.
27 10 9 cfv 
 |-  ( n ` x )
28 27 15 14 co 
 |-  ( ( n ` x ) ^ 2 )
29 11 9 cfv 
 |-  ( n ` y )
30 29 15 14 co 
 |-  ( ( n ` y ) ^ 2 )
31 28 30 17 co 
 |-  ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) )
32 15 31 26 co 
 |-  ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) )
33 25 32 wceq 
 |-  ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) )
34 33 8 7 wral 
 |-  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 ) ) )
35 34 5 7 wral 
 |-  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 ) ) )
36 35 2 3 4 coprab 
 |-  { <. <. 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 ) ) ) }
37 1 36 cin 
 |-  ( 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 ) ) ) } )
38 0 37 wceq 
 |-  CPreHilOLD = ( 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 ) ) ) } )