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

Definition df-dip 30729
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 30728 . 2 class ·𝑖OLD
2 vu . . 3 setvar 𝑢
3 cnv 30612 . . 3 class NrmCVec
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1535 . . . . 5 class 𝑢
7 cba 30614 . . . . 5 class BaseSet
86, 7cfv 6562 . . . 4 class (BaseSet‘𝑢)
9 c1 11153 . . . . . . 7 class 1
10 c4 12320 . . . . . . 7 class 4
11 cfz 13543 . . . . . . 7 class ...
129, 10, 11co 7430 . . . . . 6 class (1...4)
13 ci 11154 . . . . . . . 8 class i
14 vk . . . . . . . . 9 setvar 𝑘
1514cv 1535 . . . . . . . 8 class 𝑘
16 cexp 14098 . . . . . . . 8 class
1713, 15, 16co 7430 . . . . . . 7 class (i↑𝑘)
184cv 1535 . . . . . . . . . 10 class 𝑥
195cv 1535 . . . . . . . . . . 11 class 𝑦
20 cns 30615 . . . . . . . . . . . 12 class ·𝑠OLD
216, 20cfv 6562 . . . . . . . . . . 11 class ( ·𝑠OLD𝑢)
2217, 19, 21co 7430 . . . . . . . . . 10 class ((i↑𝑘)( ·𝑠OLD𝑢)𝑦)
23 cpv 30613 . . . . . . . . . . 11 class +𝑣
246, 23cfv 6562 . . . . . . . . . 10 class ( +𝑣𝑢)
2518, 22, 24co 7430 . . . . . . . . 9 class (𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦))
26 cnmcv 30618 . . . . . . . . . 10 class normCV
276, 26cfv 6562 . . . . . . . . 9 class (normCV𝑢)
2825, 27cfv 6562 . . . . . . . 8 class ((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))
29 c2 12318 . . . . . . . 8 class 2
3028, 29, 16co 7430 . . . . . . 7 class (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)
31 cmul 11157 . . . . . . 7 class ·
3217, 30, 31co 7430 . . . . . 6 class ((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2))
3312, 32, 14csu 15718 . . . . 5 class Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2))
34 cdiv 11917 . . . . 5 class /
3533, 10, 34co 7430 . . . 4 class 𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)) / 4)
364, 5, 8, 8, 35cmpo 7432 . . 3 class (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)) / 4))
372, 3, 36cmpt 5230 . 2 class (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)) / 4)))
381, 37wceq 1536 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  30730
  Copyright terms: Public domain W3C validator