Definition df-ip 9689

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 9688	. 2 class .i
2		vw	. . . . . . 7 set w
3	2	cv 1297	. . . . . 6 class w
4		vn	. . . . . . 7 set n
5	4	cv 1297	. . . . . 6 class n
6	3, 5	cop 3046	. . . . 5 class <.w, n>.
7		cnv 9535	. . . . 5 class NrmCVec
8	6, 7	wcel 1300	. . . 4 wff <.w, n>. e. NrmCVec
9		vp	. . . . . 6 set p
10	9	cv 1297	. . . . 5 class p
11		vx	. . . . . . . . . 10 set x
12	11	cv 1297	. . . . . . . . 9 class x
13	5	cdm 3986	. . . . . . . . 9 class dom n
14	12, 13	wcel 1300	. . . . . . . 8 wff x e. dom n
15		vy	. . . . . . . . . 10 set y
16	15	cv 1297	. . . . . . . . 9 class y
17	16, 13	wcel 1300	. . . . . . . 8 wff y e. dom n
18	14, 17	wa 240	. . . . . . 7 wff (x e. dom n /\ y e. dom n)
19		vz	. . . . . . . . 9 set z
20	19	cv 1297	. . . . . . . 8 class z
21		c1 6387	. . . . . . . . . . 11 class 1
22		c4 7147	. . . . . . . . . . 11 class 4
23		cfz 7637	. . . . . . . . . . 11 class ...
24	21, 22, 23	co 4884	. . . . . . . . . 10 class (1...4)
25		ci 6388	. . . . . . . . . . . 12 class _i
26		vk	. . . . . . . . . . . . 13 set k
27	26	cv 1297	. . . . . . . . . . . 12 class k
28		cexp 7811	. . . . . . . . . . . 12 class ^
29	25, 27, 28	co 4884	. . . . . . . . . . 11 class (_i^k)
30		c2nd 5019	. . . . . . . . . . . . . . . 16 class 2nd
31	3, 30	cfv 3998	. . . . . . . . . . . . . . 15 class (2nd` w)
32	29, 16, 31	co 4884	. . . . . . . . . . . . . 14 class ((_i^k)(2nd` w)y)
33		c1st 5018	. . . . . . . . . . . . . . 15 class 1st
34	3, 33	cfv 3998	. . . . . . . . . . . . . 14 class (1st` w)
35	12, 32, 34	co 4884	. . . . . . . . . . . . 13 class (x(1st` w)((_i^k)(2nd` w)y))
36	35, 5	cfv 3998	. . . . . . . . . . . 12 class (n` (x(1st` w)((_i^k)(2nd` w)y)))
37		c2 7145	. . . . . . . . . . . 12 class 2
38	36, 37, 28	co 4884	. . . . . . . . . . 11 class ((n` (x(1st` w)((_i^k)(2nd` w)y)))^2)
39		cmul 6391	. . . . . . . . . . 11 class x.
40	29, 38, 39	co 4884	. . . . . . . . . 10 class ((_i^k) x. ((n` (x(1st` w)((_i^k)(2nd` w)y)))^2))
41	24, 40, 26	csu 8239	. . . . . . . . 9 class sum_k e. (1...4)((_i^k) x. ((n` (x(1st` w)((_i^k)(2nd` w)y)))^2))
42		cdiv 6447	. . . . . . . . 9 class /
43	41, 22, 42	co 4884	. . . . . . . 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 1298	. . . . . . 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 240	. . . . . 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 4885	. . . . 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 1298	. . . 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 240	. . 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 4885	. 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 1298	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 9691

Copyright terms: Public domain