Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dip Structured version   Visualization version   GIF version

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 (1st ‘𝑤), the scalar product is (2nd ‘𝑤), 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
StepHypRef 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 𝑦
62cv 1537 . . . . 5 class 𝑢
7 cba 28468 . . . . 5 class BaseSet
86, 7cfv 6335 . . . 4 class (BaseSet‘𝑢)
9 c1 10576 . . . . . . 7 class 1
10 c4 11731 . . . . . . 7 class 4
11 cfz 12939 . . . . . . 7 class ...
129, 10, 11co 7150 . . . . . 6 class (1...4)
13 ci 10577 . . . . . . . 8 class i
14 vk . . . . . . . . 9 setvar 𝑘
1514cv 1537 . . . . . . . 8 class 𝑘
16 cexp 13479 . . . . . . . 8 class
1713, 15, 16co 7150 . . . . . . 7 class (i↑𝑘)
184cv 1537 . . . . . . . . . 10 class 𝑥
195cv 1537 . . . . . . . . . . 11 class 𝑦
20 cns 28469 . . . . . . . . . . . 12 class ·𝑠OLD
216, 20cfv 6335 . . . . . . . . . . 11 class ( ·𝑠OLD𝑢)
2217, 19, 21co 7150 . . . . . . . . . 10 class ((i↑𝑘)( ·𝑠OLD𝑢)𝑦)
23 cpv 28467 . . . . . . . . . . 11 class +𝑣
246, 23cfv 6335 . . . . . . . . . 10 class ( +𝑣𝑢)
2518, 22, 24co 7150 . . . . . . . . 9 class (𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦))
26 cnmcv 28472 . . . . . . . . . 10 class normCV
276, 26cfv 6335 . . . . . . . . 9 class (normCV𝑢)
2825, 27cfv 6335 . . . . . . . 8 class ((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))
29 c2 11729 . . . . . . . 8 class 2
3028, 29, 16co 7150 . . . . . . 7 class (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)
31 cmul 10580 . . . . . . 7 class ·
3217, 30, 31co 7150 . . . . . 6 class ((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2))
3312, 32, 14csu 15090 . . . . 5 class Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2))
34 cdiv 11335 . . . . 5 class /
3533, 10, 34co 7150 . . . 4 class 𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)) / 4)
364, 5, 8, 8, 35cmpo 7152 . . 3 class (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)) / 4))
372, 3, 36cmpt 5112 . 2 class (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)) / 4)))
381, 37wceq 1538 1 wff ·𝑖OLD = (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)) / 4)))
 Colors of variables: wff setvar class This definition is referenced by:  dipfval  28584
 Copyright terms: Public domain W3C validator