Definition df-dip 28583

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 28582	. 2 class ·𝑖OLD
2		vu	. . 3 setvar 𝑢
3		cnv 28466	. . 3 class NrmCVec
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1537	. . . . 5 class 𝑢
7		cba 28468	. . . . 5 class BaseSet
8	6, 7	cfv 6335	. . . 4 class (BaseSet‘𝑢)
9		c1 10576	. . . . . . 7 class 1
10		c4 11731	. . . . . . 7 class 4
11		cfz 12939	. . . . . . 7 class ...
12	9, 10, 11	co 7150	. . . . . 6 class (1...4)
13		ci 10577	. . . . . . . 8 class i
14		vk	. . . . . . . . 9 setvar 𝑘
15	14	cv 1537	. . . . . . . 8 class 𝑘
16		cexp 13479	. . . . . . . 8 class ↑
17	13, 15, 16	co 7150	. . . . . . 7 class (i↑𝑘)
18	4	cv 1537	. . . . . . . . . 10 class 𝑥
19	5	cv 1537	. . . . . . . . . . 11 class 𝑦
20		cns 28469	. . . . . . . . . . . 12 class ·𝑠OLD
21	6, 20	cfv 6335	. . . . . . . . . . 11 class ( ·𝑠OLD ‘𝑢)
22	17, 19, 21	co 7150	. . . . . . . . . 10 class ((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)
23		cpv 28467	. . . . . . . . . . 11 class +𝑣
24	6, 23	cfv 6335	. . . . . . . . . 10 class ( +𝑣 ‘𝑢)
25	18, 22, 24	co 7150	. . . . . . . . 9 class (𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦))
26		cnmcv 28472	. . . . . . . . . 10 class normCV
27	6, 26	cfv 6335	. . . . . . . . 9 class (normCV‘𝑢)
28	25, 27	cfv 6335	. . . . . . . 8 class ((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))
29		c2 11729	. . . . . . . 8 class 2
30	28, 29, 16	co 7150	. . . . . . 7 class (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)
31		cmul 10580	. . . . . . 7 class ·
32	17, 30, 31	co 7150	. . . . . 6 class ((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2))
33	12, 32, 14	csu 15090	. . . . 5 class Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2))
34		cdiv 11335	. . . . 5 class /
35	33, 10, 34	co 7150	. . . 4 class (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)
36	4, 5, 8, 8, 35	cmpo 7152	. . 3 class (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4))
37	2, 3, 36	cmpt 5112	. 2 class (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))
38	1, 37	wceq 1538	1 wff ·𝑖OLD = (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))

This definition is referenced by:  dipfval  28584