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 ) ) )