Definition df-ph 27668

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

Step	Hyp	Ref	Expression
1		ccphlo 27667	. 2 class CPreHil OLD
2		cnv 27439	. . 3 class NrmCVec
3		vx	. . . . . . . . . . . 12 setvar x
4	3	cv 1482	. . . . . . . . . . 11 class x
5		vy	. . . . . . . . . . . 12 setvar y
6	5	cv 1482	. . . . . . . . . . 11 class y
7		vg	. . . . . . . . . . . 12 setvar g
8	7	cv 1482	. . . . . . . . . . 11 class g
9	4, 6, 8	co 6650	. . . . . . . . . 10 class ( x g y )
10		vn	. . . . . . . . . . 11 setvar n
11	10	cv 1482	. . . . . . . . . 10 class n
12	9, 11	cfv 5888	. . . . . . . . 9 class ( n ` ( x g y ) )
13		c2 11070	. . . . . . . . 9 class 2
14		cexp 12860	. . . . . . . . 9 class ^
15	12, 13, 14	co 6650	. . . . . . . 8 class ( ( n ` ( x g y ) ) ^ 2 )
16		c1 9937	. . . . . . . . . . . . 13 class 1
17	16	cneg 10267	. . . . . . . . . . . 12 class -u 1
18		vs	. . . . . . . . . . . . 13 setvar s
19	18	cv 1482	. . . . . . . . . . . 12 class s
20	17, 6, 19	co 6650	. . . . . . . . . . 11 class ( -u 1 s y )
21	4, 20, 8	co 6650	. . . . . . . . . 10 class ( x g ( -u 1 s y ) )
22	21, 11	cfv 5888	. . . . . . . . 9 class ( n ` ( x g ( -u 1 s y ) ) )
23	22, 13, 14	co 6650	. . . . . . . 8 class ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 )
24		caddc 9939	. . . . . . . 8 class +
25	15, 23, 24	co 6650	. . . . . . 7 class ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) )
26	4, 11	cfv 5888	. . . . . . . . . 10 class ( n ` x )
27	26, 13, 14	co 6650	. . . . . . . . 9 class ( ( n ` x ) ^ 2 )
28	6, 11	cfv 5888	. . . . . . . . . 10 class ( n ` y )
29	28, 13, 14	co 6650	. . . . . . . . 9 class ( ( n ` y ) ^ 2 )
30	27, 29, 24	co 6650	. . . . . . . 8 class ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) )
31		cmul 9941	. . . . . . . 8 class x.
32	13, 30, 31	co 6650	. . . . . . 7 class ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) )
33	25, 32	wceq 1483	. . . . . 6 wff ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) )
34	8	crn 5115	. . . . . 6 class ran g
35	33, 5, 34	wral 2912	. . . . 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 ) ) )
36	35, 3, 34	wral 2912	. . . 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 ) ) )
37	36, 7, 18, 10	coprab 6651	. . 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 ) ) ) }
38	2, 37	cin 3573	. 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 ) ) ) } )
39	1, 38	wceq 1483	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 ) ) ) } )

This definition is referenced by:  phnv  27669  isphg  27672