Definition df-ph 22267

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 22266	. 2 class CPreHil OLD
2		cnv 22016	. . 3 class NrmCVec
3		vx	. . . . . . . . . . . 12 set x
4	3	cv 1648	. . . . . . . . . . 11 class x
5		vy	. . . . . . . . . . . 12 set y
6	5	cv 1648	. . . . . . . . . . 11 class y
7		vg	. . . . . . . . . . . 12 set g
8	7	cv 1648	. . . . . . . . . . 11 class g
9	4, 6, 8	co 6040	. . . . . . . . . 10 class ( x g y )
10		vn	. . . . . . . . . . 11 set n
11	10	cv 1648	. . . . . . . . . 10 class n
12	9, 11	cfv 5413	. . . . . . . . 9 class ( n ` ( x g y ) )
13		c2 10005	. . . . . . . . 9 class 2
14		cexp 11337	. . . . . . . . 9 class ^
15	12, 13, 14	co 6040	. . . . . . . 8 class ( ( n ` ( x g y ) ) ^ 2 )
16		c1 8947	. . . . . . . . . . . . 13 class 1
17	16	cneg 9248	. . . . . . . . . . . 12 class -u 1
18		vs	. . . . . . . . . . . . 13 set s
19	18	cv 1648	. . . . . . . . . . . 12 class s
20	17, 6, 19	co 6040	. . . . . . . . . . 11 class ( -u 1 s y )
21	4, 20, 8	co 6040	. . . . . . . . . 10 class ( x g ( -u 1 s y ) )
22	21, 11	cfv 5413	. . . . . . . . 9 class ( n ` ( x g ( -u 1 s y ) ) )
23	22, 13, 14	co 6040	. . . . . . . 8 class ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 )
24		caddc 8949	. . . . . . . 8 class +
25	15, 23, 24	co 6040	. . . . . . 7 class ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) )
26	4, 11	cfv 5413	. . . . . . . . . 10 class ( n ` x )
27	26, 13, 14	co 6040	. . . . . . . . 9 class ( ( n ` x ) ^ 2 )
28	6, 11	cfv 5413	. . . . . . . . . 10 class ( n ` y )
29	28, 13, 14	co 6040	. . . . . . . . 9 class ( ( n ` y ) ^ 2 )
30	27, 29, 24	co 6040	. . . . . . . 8 class ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) )
31		cmul 8951	. . . . . . . 8 class x.
32	13, 30, 31	co 6040	. . . . . . 7 class ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) )
33	25, 32	wceq 1649	. . . . . 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 4838	. . . . . 6 class ran g
35	33, 5, 34	wral 2666	. . . . 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 2666	. . . 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 6041	. . 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 3279	. 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 1649	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  22268  isphg  22271