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 29932
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 29931 . 2 class ·𝑖OLD
2 vu . . 3 setvar 𝑒
3 cnv 29815 . . 3 class NrmCVec
4 vx . . . 4 setvar π‘₯
5 vy . . . 4 setvar 𝑦
62cv 1541 . . . . 5 class 𝑒
7 cba 29817 . . . . 5 class BaseSet
86, 7cfv 6540 . . . 4 class (BaseSetβ€˜π‘’)
9 c1 11107 . . . . . . 7 class 1
10 c4 12265 . . . . . . 7 class 4
11 cfz 13480 . . . . . . 7 class ...
129, 10, 11co 7404 . . . . . 6 class (1...4)
13 ci 11108 . . . . . . . 8 class i
14 vk . . . . . . . . 9 setvar π‘˜
1514cv 1541 . . . . . . . 8 class π‘˜
16 cexp 14023 . . . . . . . 8 class ↑
1713, 15, 16co 7404 . . . . . . 7 class (iβ†‘π‘˜)
184cv 1541 . . . . . . . . . 10 class π‘₯
195cv 1541 . . . . . . . . . . 11 class 𝑦
20 cns 29818 . . . . . . . . . . . 12 class ·𝑠OLD
216, 20cfv 6540 . . . . . . . . . . 11 class ( ·𝑠OLD β€˜π‘’)
2217, 19, 21co 7404 . . . . . . . . . 10 class ((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)
23 cpv 29816 . . . . . . . . . . 11 class +𝑣
246, 23cfv 6540 . . . . . . . . . 10 class ( +𝑣 β€˜π‘’)
2518, 22, 24co 7404 . . . . . . . . 9 class (π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦))
26 cnmcv 29821 . . . . . . . . . 10 class normCV
276, 26cfv 6540 . . . . . . . . 9 class (normCVβ€˜π‘’)
2825, 27cfv 6540 . . . . . . . 8 class ((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))
29 c2 12263 . . . . . . . 8 class 2
3028, 29, 16co 7404 . . . . . . 7 class (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2)
31 cmul 11111 . . . . . . 7 class Β·
3217, 30, 31co 7404 . . . . . 6 class ((iβ†‘π‘˜) Β· (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2))
3312, 32, 14csu 15628 . . . . 5 class Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2))
34 cdiv 11867 . . . . 5 class /
3533, 10, 34co 7404 . . . 4 class (Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2)) / 4)
364, 5, 8, 8, 35cmpo 7406 . . 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 1542 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  29933
  Copyright terms: Public domain W3C validator