Definition df-ip 8350

Description: Define a function that maps a complex normed vector space to its inner product operation in case its norm satisfies the parallelogram identity (otherwise the operation is still defined, but not meaningful). Based on Exercise 4(a) of [ReedSimon] p. 63 and Theorem 6.44 of [Ponnusamy] p. 361. Vector addition is (1st` w), the scalar product is (2nd` w), and the norm is n.

Assertion

Ref	Expression
df-ip	|- .i = {<.<.w, n>., p>. | (<.w, n>. e. NrmCVec /\ p = {<.<.x, y>., z>. | ((x e. dom n /\ y e. dom n) /\ z = (sum_k e. (1...4)((i^k) x. ((n` (x(1st` w)((i^k)(2nd` w)y)))^2)) / 4))})}

Distinct variable group:   k,n,p,w,x,y,z

Detailed syntax breakdown of Definition df-ip

Step	Hyp	Ref	Expression
1		cip 8349	. 2 class .i
2		vw	. . . . . . 7 set w
3	2	cv 955	. . . . . 6 class w
4		vn	. . . . . . 7 set n
5	4	cv 955	. . . . . 6 class n
6	3, 5	cop 2411	. . . . 5 class <.w, n>.
7		cnv 8203	. . . . 5 class NrmCVec
8	6, 7	wcel 958	. . . 4 wff <.w, n>. e. NrmCVec
9		vp	. . . . . 6 set p
10	9	cv 955	. . . . 5 class p
11		vx	. . . . . . . . . 10 set x
12	11	cv 955	. . . . . . . . 9 class x
13	5	cdm 3170	. . . . . . . . 9 class dom n
14	12, 13	wcel 958	. . . . . . . 8 wff x e. dom n
15		vy	. . . . . . . . . 10 set y
16	15	cv 955	. . . . . . . . 9 class y
17	16, 13	wcel 958	. . . . . . . 8 wff y e. dom n
18	14, 17	wa 223	. . . . . . 7 wff (x e. dom n /\ y e. dom n)
19		vz	. . . . . . . . 9 set z
20	19	cv 955	. . . . . . . 8 class z
21		c1 5235	. . . . . . . . . . 11 class 1
22		c4 5963	. . . . . . . . . . 11 class 4
23		cfz 6467	. . . . . . . . . . 11 class ...
24	21, 22, 23	co 3963	. . . . . . . . . 10 class (1...4)
25		ci 5236	. . . . . . . . . . . 12 class i
26		vk	. . . . . . . . . . . . 13 set k
27	26	cv 955	. . . . . . . . . . . 12 class k
28		cexp 6568	. . . . . . . . . . . 12 class ^
29	25, 27, 28	co 3963	. . . . . . . . . . 11 class (i^k)
30		c2nd 4078	. . . . . . . . . . . . . . . 16 class 2nd
31	3, 30	cfv 3182	. . . . . . . . . . . . . . 15 class (2nd` w)
32	29, 16, 31	co 3963	. . . . . . . . . . . . . 14 class ((i^k)(2nd` w)y)
33		c1st 4077	. . . . . . . . . . . . . . 15 class 1st
34	3, 33	cfv 3182	. . . . . . . . . . . . . 14 class (1st` w)
35	12, 32, 34	co 3963	. . . . . . . . . . . . 13 class (x(1st` w)((i^k)(2nd` w)y))
36	35, 5	cfv 3182	. . . . . . . . . . . 12 class (n` (x(1st` w)((i^k)(2nd` w)y)))
37		c2 5961	. . . . . . . . . . . 12 class 2
38	36, 37, 28	co 3963	. . . . . . . . . . 11 class ((n` (x(1st` w)((i^k)(2nd` w)y)))^2)
39		cmul 5239	. . . . . . . . . . 11 class x.
40	29, 38, 39	co 3963	. . . . . . . . . 10 class ((i^k) x. ((n` (x(1st` w)((i^k)(2nd` w)y)))^2))
41	24, 40, 26	csu 6979	. . . . . . . . 9 class sum_k e. (1...4)((i^k) x. ((n` (x(1st` w)((i^k)(2nd` w)y)))^2))
42		cdiv 5294	. . . . . . . . 9 class /
43	41, 22, 42	co 3963	. . . . . . . 8 class (sum_k e. (1...4)((i^k) x. ((n` (x(1st` w)((i^k)(2nd` w)y)))^2)) / 4)
44	20, 43	wceq 956	. . . . . . 7 wff z = (sum_k e. (1...4)((i^k) x. ((n` (x(1st` w)((i^k)(2nd` w)y)))^2)) / 4)
45	18, 44	wa 223	. . . . . 6 wff ((x e. dom n /\ y e. dom n) /\ z = (sum_k e. (1...4)((i^k) x. ((n` (x(1st` w)((i^k)(2nd` w)y)))^2)) / 4))
46	45, 11, 15, 19	copab2 3964	. . . . 5 class {<.<.x, y>., z>. | ((x e. dom n /\ y e. dom n) /\ z = (sum_k e. (1...4)((i^k) x. ((n` (x(1st` w)((i^k)(2nd` w)y)))^2)) / 4))}
47	10, 46	wceq 956	. . . 4 wff p = {<.<.x, y>., z>. | ((x e. dom n /\ y e. dom n) /\ z = (sum_k e. (1...4)((i^k) x. ((n` (x(1st` w)((i^k)(2nd` w)y)))^2)) / 4))}
48	8, 47	wa 223	. . 3 wff (<.w, n>. e. NrmCVec /\ p = {<.<.x, y>., z>. | ((x e. dom n /\ y e. dom n) /\ z = (sum_k e. (1...4)((i^k) x. ((n` (x(1st` w)((i^k)(2nd` w)y)))^2)) / 4))})
49	48, 2, 4, 9	copab2 3964	. 2 class {<.<.w, n>., p>. | (<.w, n>. e. NrmCVec /\ p = {<.<.x, y>., z>. | ((x e. dom n /\ y e. dom n) /\ z = (sum_k e. (1...4)((i^k) x. ((n` (x(1st` w)((i^k)(2nd` w)y)))^2)) / 4))})}
50	1, 49	wceq 956	1 wff .i = {<.<.w, n>., p>. | (<.w, n>. e. NrmCVec /\ p = {<.<.x, y>., z>. | ((x e. dom n /\ y e. dom n) /\ z = (sum_k e. (1...4)((i^k) x. ((n` (x(1st` w)((i^k)(2nd` w)y)))^2)) / 4))})}

This definition is referenced by:  ipfval 8352

Copyright terms: Public domain