Definition df-ph 27052

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 𝑔, the scalar product is 𝑠, and the norm is 𝑛. 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	⊢ CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))})

Distinct variable group:   𝑔,𝑛,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-ph

Step	Hyp	Ref	Expression
1		ccphlo 27051	. 2 class CPreHilOLD
2		cnv 26823	. . 3 class NrmCVec
3		vx	. . . . . . . . . . . 12 setvar 𝑥
4	3	cv 1474	. . . . . . . . . . 11 class 𝑥
5		vy	. . . . . . . . . . . 12 setvar 𝑦
6	5	cv 1474	. . . . . . . . . . 11 class 𝑦
7		vg	. . . . . . . . . . . 12 setvar 𝑔
8	7	cv 1474	. . . . . . . . . . 11 class 𝑔
9	4, 6, 8	co 6549	. . . . . . . . . 10 class (𝑥𝑔𝑦)
10		vn	. . . . . . . . . . 11 setvar 𝑛
11	10	cv 1474	. . . . . . . . . 10 class 𝑛
12	9, 11	cfv 5804	. . . . . . . . 9 class (𝑛‘(𝑥𝑔𝑦))
13		c2 10947	. . . . . . . . 9 class 2
14		cexp 12722	. . . . . . . . 9 class ↑
15	12, 13, 14	co 6549	. . . . . . . 8 class ((𝑛‘(𝑥𝑔𝑦))↑2)
16		c1 9816	. . . . . . . . . . . . 13 class 1
17	16	cneg 10146	. . . . . . . . . . . 12 class -1
18		vs	. . . . . . . . . . . . 13 setvar 𝑠
19	18	cv 1474	. . . . . . . . . . . 12 class 𝑠
20	17, 6, 19	co 6549	. . . . . . . . . . 11 class (-1𝑠𝑦)
21	4, 20, 8	co 6549	. . . . . . . . . 10 class (𝑥𝑔(-1𝑠𝑦))
22	21, 11	cfv 5804	. . . . . . . . 9 class (𝑛‘(𝑥𝑔(-1𝑠𝑦)))
23	22, 13, 14	co 6549	. . . . . . . 8 class ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)
24		caddc 9818	. . . . . . . 8 class +
25	15, 23, 24	co 6549	. . . . . . 7 class (((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2))
26	4, 11	cfv 5804	. . . . . . . . . 10 class (𝑛‘𝑥)
27	26, 13, 14	co 6549	. . . . . . . . 9 class ((𝑛‘𝑥)↑2)
28	6, 11	cfv 5804	. . . . . . . . . 10 class (𝑛‘𝑦)
29	28, 13, 14	co 6549	. . . . . . . . 9 class ((𝑛‘𝑦)↑2)
30	27, 29, 24	co 6549	. . . . . . . 8 class (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2))
31		cmul 9820	. . . . . . . 8 class ·
32	13, 30, 31	co 6549	. . . . . . 7 class (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))
33	25, 32	wceq 1475	. . . . . 6 wff (((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))
34	8	crn 5039	. . . . . 6 class ran 𝑔
35	33, 5, 34	wral 2896	. . . . 5 wff ∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))
36	35, 3, 34	wral 2896	. . . 4 wff ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))
37	36, 7, 18, 10	coprab 6550	. . 3 class {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))}
38	2, 37	cin 3539	. 2 class (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))})
39	1, 38	wceq 1475	1 wff CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))})

This definition is referenced by:  phnv  27053  isphg  27056