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 27884
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 27883 . 2 class ·𝑖OLD
2 vu . . 3 setvar 𝑢
3 cnv 27767 . . 3 class NrmCVec
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1636 . . . . 5 class 𝑢
7 cba 27769 . . . . 5 class BaseSet
86, 7cfv 6101 . . . 4 class (BaseSet‘𝑢)
9 c1 10222 . . . . . . 7 class 1
10 c4 11358 . . . . . . 7 class 4
11 cfz 12549 . . . . . . 7 class ...
129, 10, 11co 6874 . . . . . 6 class (1...4)
13 ci 10223 . . . . . . . 8 class i
14 vk . . . . . . . . 9 setvar 𝑘
1514cv 1636 . . . . . . . 8 class 𝑘
16 cexp 13083 . . . . . . . 8 class
1713, 15, 16co 6874 . . . . . . 7 class (i↑𝑘)
184cv 1636 . . . . . . . . . 10 class 𝑥
195cv 1636 . . . . . . . . . . 11 class 𝑦
20 cns 27770 . . . . . . . . . . . 12 class ·𝑠OLD
216, 20cfv 6101 . . . . . . . . . . 11 class ( ·𝑠OLD𝑢)
2217, 19, 21co 6874 . . . . . . . . . 10 class ((i↑𝑘)( ·𝑠OLD𝑢)𝑦)
23 cpv 27768 . . . . . . . . . . 11 class +𝑣
246, 23cfv 6101 . . . . . . . . . 10 class ( +𝑣𝑢)
2518, 22, 24co 6874 . . . . . . . . 9 class (𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦))
26 cnmcv 27773 . . . . . . . . . 10 class normCV
276, 26cfv 6101 . . . . . . . . 9 class (normCV𝑢)
2825, 27cfv 6101 . . . . . . . 8 class ((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))
29 c2 11356 . . . . . . . 8 class 2
3028, 29, 16co 6874 . . . . . . 7 class (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)
31 cmul 10226 . . . . . . 7 class ·
3217, 30, 31co 6874 . . . . . 6 class ((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2))
3312, 32, 14csu 14639 . . . . 5 class Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2))
34 cdiv 10969 . . . . 5 class /
3533, 10, 34co 6874 . . . 4 class 𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)) / 4)
364, 5, 8, 8, 35cmpt2 6876 . . 3 class (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)) / 4))
372, 3, 36cmpt 4923 . 2 class (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV𝑢)‘(𝑥( +𝑣𝑢)((i↑𝑘)( ·𝑠OLD𝑢)𝑦)))↑2)) / 4)))
381, 37wceq 1637 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  27885
  Copyright terms: Public domain W3C validator