Definition df-dip 30505

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 30504	. 2 class ·𝑖OLD
2		vu	. . 3 setvar 𝑢
3		cnv 30388	. . 3 class NrmCVec
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1533	. . . . 5 class 𝑢
7		cba 30390	. . . . 5 class BaseSet
8	6, 7	cfv 6543	. . . 4 class (BaseSet‘𝑢)
9		c1 11134	. . . . . . 7 class 1
10		c4 12294	. . . . . . 7 class 4
11		cfz 13511	. . . . . . 7 class ...
12	9, 10, 11	co 7415	. . . . . 6 class (1...4)
13		ci 11135	. . . . . . . 8 class i
14		vk	. . . . . . . . 9 setvar 𝑘
15	14	cv 1533	. . . . . . . 8 class 𝑘
16		cexp 14053	. . . . . . . 8 class ↑
17	13, 15, 16	co 7415	. . . . . . 7 class (i↑𝑘)
18	4	cv 1533	. . . . . . . . . 10 class 𝑥
19	5	cv 1533	. . . . . . . . . . 11 class 𝑦
20		cns 30391	. . . . . . . . . . . 12 class ·𝑠OLD
21	6, 20	cfv 6543	. . . . . . . . . . 11 class ( ·𝑠OLD ‘𝑢)
22	17, 19, 21	co 7415	. . . . . . . . . 10 class ((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)
23		cpv 30389	. . . . . . . . . . 11 class +𝑣
24	6, 23	cfv 6543	. . . . . . . . . 10 class ( +𝑣 ‘𝑢)
25	18, 22, 24	co 7415	. . . . . . . . 9 class (𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦))
26		cnmcv 30394	. . . . . . . . . 10 class normCV
27	6, 26	cfv 6543	. . . . . . . . 9 class (normCV‘𝑢)
28	25, 27	cfv 6543	. . . . . . . 8 class ((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))
29		c2 12292	. . . . . . . 8 class 2
30	28, 29, 16	co 7415	. . . . . . 7 class (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)
31		cmul 11138	. . . . . . 7 class ·
32	17, 30, 31	co 7415	. . . . . 6 class ((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2))
33	12, 32, 14	csu 15659	. . . . 5 class Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2))
34		cdiv 11896	. . . . 5 class /
35	33, 10, 34	co 7415	. . . 4 class (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)
36	4, 5, 8, 8, 35	cmpo 7417	. . 3 class (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4))
37	2, 3, 36	cmpt 5226	. 2 class (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))
38	1, 37	wceq 1534	1 wff ·𝑖OLD = (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))

This definition is referenced by:  dipfval  30506

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »