This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-dip

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 ( 1stw ) , the scalar product is ( 2ndw ) , and the norm is n . (Contributed by NM, 10-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion df-dip ·𝑖OLD = ( 𝑢 ∈ NrmCVec ↦ ( 𝑥 ∈ ( BaseSet ‘ 𝑢 ) , 𝑦 ∈ ( BaseSet ‘ 𝑢 ) ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdip ⊢ ·𝑖OLD
1 vu ⊢ 𝑢
2 cnv ⊢ NrmCVec
3 vx ⊢ 𝑥
4 cba ⊢ BaseSet
5 1 cv ⊢ 𝑢
6 5 4 cfv ⊢ ( BaseSet ‘ 𝑢 )
7 vy ⊢ 𝑦
8 vk ⊢ 𝑘
9 c1 ⊢ 1
10 cfz ⊢ ...
11 c4 ⊢ 4
12 9 11 10 co ⊢ ( 1 ... 4 )
13 ci ⊢ i
14 cexp ⊢ ↑
15 8 cv ⊢ 𝑘
16 13 15 14 co ⊢ ( i ↑ 𝑘 )
17 cmul ⊢ ·
18 cnmcv ⊢ normCV
19 5 18 cfv ⊢ ( normCV ‘ 𝑢 )
20 3 cv ⊢ 𝑥
21 cpv ⊢ +𝑣
22 5 21 cfv ⊢ ( +𝑣 ‘ 𝑢 )
23 cns ⊢ ·𝑠OLD
24 5 23 cfv ⊢ ( ·𝑠OLD ‘ 𝑢 )
25 7 cv ⊢ 𝑦
26 16 25 24 co ⊢ ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 )
27 20 26 22 co ⊢ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) )
28 27 19 cfv ⊢ ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) )
29 c2 ⊢ 2
30 28 29 14 co ⊢ ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 )
31 16 30 17 co ⊢ ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) )
32 12 31 8 csu ⊢ Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) )
33 cdiv ⊢ /
34 32 11 33 co ⊢ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 )
35 3 7 6 6 34 cmpo ⊢ ( 𝑥 ∈ ( BaseSet ‘ 𝑢 ) , 𝑦 ∈ ( BaseSet ‘ 𝑢 ) ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) )
36 1 2 35 cmpt ⊢ ( 𝑢 ∈ NrmCVec ↦ ( 𝑥 ∈ ( BaseSet ‘ 𝑢 ) , 𝑦 ∈ ( BaseSet ‘ 𝑢 ) ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) )
37 0 36 wceq ⊢ ·𝑖OLD = ( 𝑢 ∈ NrmCVec ↦ ( 𝑥 ∈ ( BaseSet ‘ 𝑢 ) , 𝑦 ∈ ( BaseSet ‘ 𝑢 ) ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑢 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑢 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) )