Definition df-dip 31309

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 31308	. 2 class ·𝑖OLD
2		vu	. . 3 setvar 𝑢
3		cnv 31192	. . 3 class NrmCVec
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1568	. . . . 5 class 𝑢
7		cba 31194	. . . . 5 class BaseSet
8	6, 7	cfv 6539	. . . 4 class (BaseSet‘𝑢)
9		c1 11205	. . . . . . 7 class 1
10		c4 12403	. . . . . . 7 class 4
11		cfz 13643	. . . . . . 7 class ...
12	9, 10, 11	co 7421	. . . . . 6 class (1...4)
13		ci 11206	. . . . . . . 8 class i
14		vk	. . . . . . . . 9 setvar 𝑘
15	14	cv 1568	. . . . . . . 8 class 𝑘
16		cexp 14208	. . . . . . . 8 class ↑
17	13, 15, 16	co 7421	. . . . . . 7 class (i↑𝑘)
18	4	cv 1568	. . . . . . . . . 10 class 𝑥
19	5	cv 1568	. . . . . . . . . . 11 class 𝑦
20		cns 31195	. . . . . . . . . . . 12 class ·𝑠OLD
21	6, 20	cfv 6539	. . . . . . . . . . 11 class ( ·𝑠OLD ‘𝑢)
22	17, 19, 21	co 7421	. . . . . . . . . 10 class ((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)
23		cpv 31193	. . . . . . . . . . 11 class +𝑣
24	6, 23	cfv 6539	. . . . . . . . . 10 class ( +𝑣 ‘𝑢)
25	18, 22, 24	co 7421	. . . . . . . . 9 class (𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦))
26		cnmcv 31198	. . . . . . . . . 10 class normCV
27	6, 26	cfv 6539	. . . . . . . . 9 class (normCV‘𝑢)
28	25, 27	cfv 6539	. . . . . . . 8 class ((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))
29		c2 12401	. . . . . . . 8 class 2
30	28, 29, 16	co 7421	. . . . . . 7 class (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)
31		cmul 11209	. . . . . . 7 class ·
32	17, 30, 31	co 7421	. . . . . 6 class ((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2))
33	12, 32, 14	csu 15859	. . . . 5 class Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2))
34		cdiv 11977	. . . . 5 class /
35	33, 10, 34	co 7421	. . . 4 class (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)
36	4, 5, 8, 8, 35	cmpo 7423	. . 3 class (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4))
37	2, 3, 36	cmpt 5185	. 2 class (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))
38	1, 37	wceq 1569	1 wff ·𝑖OLD = (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))

This definition is used by:  dipfval  31310