Definition df-dip 27556

Description: Define a function that maps a normed complex 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. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.)

Assertion

Ref	Expression
df-dip	|- .iOLD = ( u e. NrmCVec |-> ( x e. ( BaseSet ` u ) , y e. ( BaseSet ` u ) |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) ) / 4 ) ) )

Distinct variable group:   u, k, x, y

Detailed syntax breakdown of Definition df-dip

Step	Hyp	Ref	Expression
1		cdip 27555	. 2 class .iOLD
2		vu	. . 3 setvar u
3		cnv 27439	. . 3 class NrmCVec
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1482	. . . . 5 class u
7		cba 27441	. . . . 5 class BaseSet
8	6, 7	cfv 5888	. . . 4 class ( BaseSet ` u )
9		c1 9937	. . . . . . 7 class 1
10		c4 11072	. . . . . . 7 class 4
11		cfz 12326	. . . . . . 7 class ...
12	9, 10, 11	co 6650	. . . . . 6 class ( 1 ... 4 )
13		ci 9938	. . . . . . . 8 class _i
14		vk	. . . . . . . . 9 setvar k
15	14	cv 1482	. . . . . . . 8 class k
16		cexp 12860	. . . . . . . 8 class ^
17	13, 15, 16	co 6650	. . . . . . 7 class ( _i ^ k )
18	4	cv 1482	. . . . . . . . . 10 class x
19	5	cv 1482	. . . . . . . . . . 11 class y
20		cns 27442	. . . . . . . . . . . 12 class .sOLD
21	6, 20	cfv 5888	. . . . . . . . . . 11 class ( .sOLD ` u )
22	17, 19, 21	co 6650	. . . . . . . . . 10 class ( ( _i ^ k ) ( .sOLD ` u ) y )
23		cpv 27440	. . . . . . . . . . 11 class +v
24	6, 23	cfv 5888	. . . . . . . . . 10 class ( +v ` u )
25	18, 22, 24	co 6650	. . . . . . . . 9 class ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) )
26		cnmcv 27445	. . . . . . . . . 10 class normCV
27	6, 26	cfv 5888	. . . . . . . . 9 class ( normCV ` u )
28	25, 27	cfv 5888	. . . . . . . 8 class ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) )
29		c2 11070	. . . . . . . 8 class 2
30	28, 29, 16	co 6650	. . . . . . 7 class ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 )
31		cmul 9941	. . . . . . 7 class x.
32	17, 30, 31	co 6650	. . . . . 6 class ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) )
33	12, 32, 14	csu 14416	. . . . 5 class sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) )
34		cdiv 10684	. . . . 5 class /
35	33, 10, 34	co 6650	. . . 4 class ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) ) / 4 )
36	4, 5, 8, 8, 35	cmpt2 6652	. . 3 class ( x e. ( BaseSet ` u ) , y e. ( BaseSet ` u ) |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) ) / 4 ) )
37	2, 3, 36	cmpt 4729	. 2 class ( u e. NrmCVec |-> ( x e. ( BaseSet ` u ) , y e. ( BaseSet ` u ) |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) ) / 4 ) ) )
38	1, 37	wceq 1483	1 wff .iOLD = ( u e. NrmCVec |-> ( x e. ( BaseSet ` u ) , y e. ( BaseSet ` u ) |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) ) / 4 ) ) )

This definition is referenced by:  dipfval  27557