Definition df-dip 31082

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 31081	. 2 class ·𝑖OLD
2		vu	. . 3 setvar 𝑢
3		cnv 30965	. . 3 class NrmCVec
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1569	. . . . 5 class 𝑢
7		cba 30967	. . . . 5 class BaseSet
8	6, 7	cfv 6540	. . . 4 class (BaseSet‘𝑢)
9		c1 11112	. . . . . . 7 class 1
10		c4 12308	. . . . . . 7 class 4
11		cfz 13546	. . . . . . 7 class ...
12	9, 10, 11	co 7416	. . . . . 6 class (1...4)
13		ci 11113	. . . . . . . 8 class i
14		vk	. . . . . . . . 9 setvar 𝑘
15	14	cv 1569	. . . . . . . 8 class 𝑘
16		cexp 14110	. . . . . . . 8 class ↑
17	13, 15, 16	co 7416	. . . . . . 7 class (i↑𝑘)
18	4	cv 1569	. . . . . . . . . 10 class 𝑥
19	5	cv 1569	. . . . . . . . . . 11 class 𝑦
20		cns 30968	. . . . . . . . . . . 12 class ·𝑠OLD
21	6, 20	cfv 6540	. . . . . . . . . . 11 class ( ·𝑠OLD ‘𝑢)
22	17, 19, 21	co 7416	. . . . . . . . . 10 class ((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)
23		cpv 30966	. . . . . . . . . . 11 class +𝑣
24	6, 23	cfv 6540	. . . . . . . . . 10 class ( +𝑣 ‘𝑢)
25	18, 22, 24	co 7416	. . . . . . . . 9 class (𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦))
26		cnmcv 30971	. . . . . . . . . 10 class normCV
27	6, 26	cfv 6540	. . . . . . . . 9 class (normCV‘𝑢)
28	25, 27	cfv 6540	. . . . . . . 8 class ((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))
29		c2 12306	. . . . . . . 8 class 2
30	28, 29, 16	co 7416	. . . . . . 7 class (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)
31		cmul 11116	. . . . . . 7 class ·
32	17, 30, 31	co 7416	. . . . . 6 class ((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2))
33	12, 32, 14	csu 15756	. . . . 5 class Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2))
34		cdiv 11882	. . . . 5 class /
35	33, 10, 34	co 7416	. . . 4 class (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)
36	4, 5, 8, 8, 35	cmpo 7418	. . 3 class (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4))
37	2, 3, 36	cmpt 5194	. 2 class (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))
38	1, 37	wceq 1570	1 wff ·𝑖OLD = (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))

This definition is used by:  dipfval  31083