Definition df-dip 30797

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 (1^st ‘𝑤), the scalar product is (2^nd ‘𝑤), and the norm is 𝑛. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.)

Assertion

Ref	Expression
df-dip	⊢ ·𝑖OLD = (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))

Distinct variable group:   𝑢,𝑘,𝑥,𝑦

Detailed syntax breakdown of Definition df-dip

Step	Hyp	Ref	Expression
1		cdip 30796	. 2 class ·𝑖OLD
2		vu	. . 3 setvar 𝑢
3		cnv 30680	. . 3 class NrmCVec
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1546	. . . . 5 class 𝑢
7		cba 30682	. . . . 5 class BaseSet
8	6, 7	cfv 6492	. . . 4 class (BaseSet‘𝑢)
9		c1 11037	. . . . . . 7 class 1
10		c4 12236	. . . . . . 7 class 4
11		cfz 13459	. . . . . . 7 class ...
12	9, 10, 11	co 7363	. . . . . 6 class (1...4)
13		ci 11038	. . . . . . . 8 class i
14		vk	. . . . . . . . 9 setvar 𝑘
15	14	cv 1546	. . . . . . . 8 class 𝑘
16		cexp 14021	. . . . . . . 8 class ↑
17	13, 15, 16	co 7363	. . . . . . 7 class (i↑𝑘)
18	4	cv 1546	. . . . . . . . . 10 class 𝑥
19	5	cv 1546	. . . . . . . . . . 11 class 𝑦
20		cns 30683	. . . . . . . . . . . 12 class ·𝑠OLD
21	6, 20	cfv 6492	. . . . . . . . . . 11 class ( ·𝑠OLD ‘𝑢)
22	17, 19, 21	co 7363	. . . . . . . . . 10 class ((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)
23		cpv 30681	. . . . . . . . . . 11 class +𝑣
24	6, 23	cfv 6492	. . . . . . . . . 10 class ( +𝑣 ‘𝑢)
25	18, 22, 24	co 7363	. . . . . . . . 9 class (𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦))
26		cnmcv 30686	. . . . . . . . . 10 class normCV
27	6, 26	cfv 6492	. . . . . . . . 9 class (normCV‘𝑢)
28	25, 27	cfv 6492	. . . . . . . 8 class ((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))
29		c2 12234	. . . . . . . 8 class 2
30	28, 29, 16	co 7363	. . . . . . 7 class (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)
31		cmul 11041	. . . . . . 7 class ·
32	17, 30, 31	co 7363	. . . . . 6 class ((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2))
33	12, 32, 14	csu 15646	. . . . 5 class Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2))
34		cdiv 11805	. . . . 5 class /
35	33, 10, 34	co 7363	. . . 4 class (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)
36	4, 5, 8, 8, 35	cmpo 7365	. . 3 class (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4))
37	2, 3, 36	cmpt 5160	. 2 class (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))
38	1, 37	wceq 1547	1 wff ·𝑖OLD = (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))

This definition is referenced by:  dipfval  30798