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	$⊢ {CPreHil}_{OLD} = NrmCVec \cap \{⟨⟨g, s⟩, n⟩ \| \forall x \in ran g \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccphlo	$class {CPreHil}_{OLD}$
1		cnv	$class NrmCVec$
2		vg	$setvar g$
3		vs	$setvar s$
4		vn	$setvar n$
5		vx	$setvar x$
6	2	cv	$setvar g$
7	6	crn	$class ran g$
8		vy	$setvar y$
9	4	cv	$setvar n$
10	5	cv	$setvar x$
11	8	cv	$setvar y$
12	10 11 6	co	$class (x g y)$
13	12 9	cfv	$class n (x g y)$
14		cexp	$class^$
15		c2	$class 2$
16	13 15 14	co	$class {n (x g y)}^{2}$
17		caddc	$class +$
18		c1	$class 1$
19	18	cneg	$class -1$
20	3	cv	$setvar s$
21	19 11 20	co	$class (-1 s y)$
22	10 21 6	co	$class (x g (-1 s y))$
23	22 9	cfv	$class n (x g (-1 s y))$
24	23 15 14	co	$class {n (x g (-1 s y))}^{2}$
25	16 24 17	co	$class ({n (x g y)}^{2} + {n (x g (-1 s y))}^{2})$
26		cmul	$class \times$
27	10 9	cfv	$class n (x)$
28	27 15 14	co	$class {n (x)}^{2}$
29	11 9	cfv	$class n (y)$
30	29 15 14	co	$class {n (y)}^{2}$
31	28 30 17	co	$class ({n (x)}^{2} + {n (y)}^{2})$
32	15 31 26	co	$class 2 ({n (x)}^{2} + {n (y)}^{2})$
33	25 32	wceq	$wff {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})$
34	33 8 7	wral	$wff \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})$
35	34 5 7	wral	$wff \forall x \in ran g \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})$
36	35 2 3 4	coprab	$class \{⟨⟨g, s⟩, n⟩ \| \forall x \in ran g \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})\}$
37	1 36	cin	$class (NrmCVec \cap \{⟨⟨g, s⟩, n⟩ \| \forall x \in ran g \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})\})$
38	0 37	wceq	$wff {CPreHil}_{OLD} = NrmCVec \cap \{⟨⟨g, s⟩, n⟩ \| \forall x \in ran g \forall y \in ran g {n (x g y)}^{2} + {n (x g (-1 s y))}^{2} = 2 ({n (x)}^{2} + {n (y)}^{2})\}$

Metamath Proof Explorer

Definition df-ph

Detailed syntax breakdown