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 29985
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 29984 . 2 class ·𝑖OLD
2 vu . . 3 setvar 𝑒
3 cnv 29868 . . 3 class NrmCVec
4 vx . . . 4 setvar π‘₯
5 vy . . . 4 setvar 𝑦
62cv 1541 . . . . 5 class 𝑒
7 cba 29870 . . . . 5 class BaseSet
86, 7cfv 6544 . . . 4 class (BaseSetβ€˜π‘’)
9 c1 11111 . . . . . . 7 class 1
10 c4 12269 . . . . . . 7 class 4
11 cfz 13484 . . . . . . 7 class ...
129, 10, 11co 7409 . . . . . 6 class (1...4)
13 ci 11112 . . . . . . . 8 class i
14 vk . . . . . . . . 9 setvar π‘˜
1514cv 1541 . . . . . . . 8 class π‘˜
16 cexp 14027 . . . . . . . 8 class ↑
1713, 15, 16co 7409 . . . . . . 7 class (iβ†‘π‘˜)
184cv 1541 . . . . . . . . . 10 class π‘₯
195cv 1541 . . . . . . . . . . 11 class 𝑦
20 cns 29871 . . . . . . . . . . . 12 class ·𝑠OLD
216, 20cfv 6544 . . . . . . . . . . 11 class ( ·𝑠OLD β€˜π‘’)
2217, 19, 21co 7409 . . . . . . . . . 10 class ((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)
23 cpv 29869 . . . . . . . . . . 11 class +𝑣
246, 23cfv 6544 . . . . . . . . . 10 class ( +𝑣 β€˜π‘’)
2518, 22, 24co 7409 . . . . . . . . 9 class (π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦))
26 cnmcv 29874 . . . . . . . . . 10 class normCV
276, 26cfv 6544 . . . . . . . . 9 class (normCVβ€˜π‘’)
2825, 27cfv 6544 . . . . . . . 8 class ((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))
29 c2 12267 . . . . . . . 8 class 2
3028, 29, 16co 7409 . . . . . . 7 class (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2)
31 cmul 11115 . . . . . . 7 class Β·
3217, 30, 31co 7409 . . . . . 6 class ((iβ†‘π‘˜) Β· (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2))
3312, 32, 14csu 15632 . . . . 5 class Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2))
34 cdiv 11871 . . . . 5 class /
3533, 10, 34co 7409 . . . 4 class (Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2)) / 4)
364, 5, 8, 8, 35cmpo 7411 . . 3 class (π‘₯ ∈ (BaseSetβ€˜π‘’), 𝑦 ∈ (BaseSetβ€˜π‘’) ↦ (Ξ£π‘˜ ∈ (1...4)((iβ†‘π‘˜) Β· (((normCVβ€˜π‘’)β€˜(π‘₯( +𝑣 β€˜π‘’)((iβ†‘π‘˜)( ·𝑠OLD β€˜π‘’)𝑦)))↑2)) / 4))
372, 3, 36cmpt 5232 . 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  29986
  Copyright terms: Public domain W3C validator