Metamath Proof Explorer

Definition df-ph

Description: Define the class of all complex inner product spaces. An inner product space is a normed vector space whose norm satisfies the parallelogram law (a property that induces an inner product). Based on Exercise 4(b) of ReedSimon p. 63. The vector operation is g , the scalar product is s , and the norm is n . An inner product space is also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion df-ph CPreHilOLD = ( NrmCVec ∩ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccphlo ⊢ CPreHilOLD
1 cnv ⊢ NrmCVec
2 vg ⊢ 𝑔
3 vs ⊢ 𝑠
4 vn ⊢ 𝑛
5 vx ⊢ 𝑥
6 2 cv ⊢ 𝑔
7 6 crn ⊢ ran 𝑔
8 vy ⊢ 𝑦
9 4 cv ⊢ 𝑛
10 5 cv ⊢ 𝑥
11 8 cv ⊢ 𝑦
12 10 11 6 co ⊢ ( 𝑥 𝑔 𝑦 )
13 12 9 cfv ⊢ ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) )
14 cexp ⊢ ↑
15 c2 ⊢ 2
16 13 15 14 co ⊢ ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 )
17 caddc ⊢ +
18 c1 ⊢ 1
19 18 cneg ⊢ - 1
20 3 cv ⊢ 𝑠
21 19 11 20 co ⊢ ( - 1 𝑠 𝑦 )
22 10 21 6 co ⊢ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) )
23 22 9 cfv ⊢ ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) )
24 23 15 14 co ⊢ ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 )
25 16 24 17 co ⊢ ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) )
26 cmul ⊢ ·
27 10 9 cfv ⊢ ( 𝑛 ‘ 𝑥 )
28 27 15 14 co ⊢ ( ( 𝑛 ‘ 𝑥 ) ↑ 2 )
29 11 9 cfv ⊢ ( 𝑛 ‘ 𝑦 )
30 29 15 14 co ⊢ ( ( 𝑛 ‘ 𝑦 ) ↑ 2 )
31 28 30 17 co ⊢ ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) )
32 15 31 26 co ⊢ ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) )
33 25 32 wceq ⊢ ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) )
34 33 8 7 wral ⊢ ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) )
35 34 5 7 wral ⊢ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) )
36 35 2 3 4 coprab ⊢ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) }
37 1 36 cin ⊢ ( NrmCVec ∩ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) } )
38 0 37 wceq ⊢ CPreHilOLD = ( NrmCVec ∩ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ↑ 2 ) + ( ( 𝑛 ‘ ( 𝑥 𝑔 ( - 1 𝑠 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑛 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝑛 ‘ 𝑦 ) ↑ 2 ) ) ) } )