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