Definition df-ph 10836

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.

Assertion

Ref	Expression
df-ph	|- CPreHil = (NrmCVec i^i {<.<.g, s>., n>. | A.x e. ran gA.y e. ran g(((n` (xgy))^2) + ((n` (xg(-u1sy)))^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		cphl 10835	. 2 class CPreHil
2		cnv 10556	. . 3 class NrmCVec
3		vx	. . . . . . . . . . . 12 set x
4	3	cv 1614	. . . . . . . . . . 11 class x
5		vy	. . . . . . . . . . . 12 set y
6	5	cv 1614	. . . . . . . . . . 11 class y
7		vg	. . . . . . . . . . . 12 set g
8	7	cv 1614	. . . . . . . . . . 11 class g
9	4, 6, 8	co 5020	. . . . . . . . . 10 class (xgy)
10		vn	. . . . . . . . . . 11 set n
11	10	cv 1614	. . . . . . . . . 10 class n
12	9, 11	cfv 4163	. . . . . . . . 9 class (n` (xgy))
13		c2 7580	. . . . . . . . 9 class 2
14		cexp 8311	. . . . . . . . 9 class ^
15	12, 13, 14	co 5020	. . . . . . . 8 class ((n` (xgy))^2)
16		c1 6830	. . . . . . . . . . . . 13 class 1
17	16	cneg 7092	. . . . . . . . . . . 12 class -u1
18		vs	. . . . . . . . . . . . 13 set s
19	18	cv 1614	. . . . . . . . . . . 12 class s
20	17, 6, 19	co 5020	. . . . . . . . . . 11 class (-u1sy)
21	4, 20, 8	co 5020	. . . . . . . . . 10 class (xg(-u1sy))
22	21, 11	cfv 4163	. . . . . . . . 9 class (n` (xg(-u1sy)))
23	22, 13, 14	co 5020	. . . . . . . 8 class ((n` (xg(-u1sy)))^2)
24		caddc 6832	. . . . . . . 8 class +
25	15, 23, 24	co 5020	. . . . . . 7 class (((n` (xgy))^2) + ((n` (xg(-u1sy)))^2))
26	4, 11	cfv 4163	. . . . . . . . . 10 class (n` x)
27	26, 13, 14	co 5020	. . . . . . . . 9 class ((n` x)^2)
28	6, 11	cfv 4163	. . . . . . . . . 10 class (n` y)
29	28, 13, 14	co 5020	. . . . . . . . 9 class ((n` y)^2)
30	27, 29, 24	co 5020	. . . . . . . 8 class (((n` x)^2) + ((n` y)^2))
31		cmul 6834	. . . . . . . 8 class x.
32	13, 30, 31	co 5020	. . . . . . 7 class (2 x. (((n` x)^2) + ((n` y)^2)))
33	25, 32	wceq 1615	. . . . . 6 wff (((n` (xgy))^2) + ((n` (xg(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2)))
34	8	crn 4152	. . . . . 6 class ran g
35	33, 5, 34	wral 2385	. . . . 5 wff A.y e. ran g(((n` (xgy))^2) + ((n` (xg(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2)))
36	35, 3, 34	wral 2385	. . . 4 wff A.x e. ran gA.y e. ran g(((n` (xgy))^2) + ((n` (xg(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2)))
37	36, 7, 18, 10	copab2 5021	. . 3 class {<.<.g, s>., n>. | A.x e. ran gA.y e. ran g(((n` (xgy))^2) + ((n` (xg(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2)))}
38	2, 37	cin 2858	. 2 class (NrmCVec i^i {<.<.g, s>., n>. | A.x e. ran gA.y e. ran g(((n` (xgy))^2) + ((n` (xg(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2)))})
39	1, 38	wceq 1615	1 wff CPreHil = (NrmCVec i^i {<.<.g, s>., n>. | A.x e. ran gA.y e. ran g(((n` (xgy))^2) + ((n` (xg(-u1sy)))^2)) = (2 x. (((n` x)^2) + ((n` y)^2)))})

This definition is referenced by:  phnv 10837  isphg 10840

Copyright terms: Public domain