MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ph Structured version   Visualization version   GIF version

Definition df-ph 28760
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 𝑔, the scalar product is 𝑠, and the norm is 𝑛. An inner product space is also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.)
Assertion
Ref Expression
df-ph CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))})
Distinct variable group:   𝑔,𝑛,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-ph
StepHypRef Expression
1 ccphlo 28759 . 2 class CPreHilOLD
2 cnv 28531 . . 3 class NrmCVec
3 vx . . . . . . . . . . . 12 setvar 𝑥
43cv 1541 . . . . . . . . . . 11 class 𝑥
5 vy . . . . . . . . . . . 12 setvar 𝑦
65cv 1541 . . . . . . . . . . 11 class 𝑦
7 vg . . . . . . . . . . . 12 setvar 𝑔
87cv 1541 . . . . . . . . . . 11 class 𝑔
94, 6, 8co 7182 . . . . . . . . . 10 class (𝑥𝑔𝑦)
10 vn . . . . . . . . . . 11 setvar 𝑛
1110cv 1541 . . . . . . . . . 10 class 𝑛
129, 11cfv 6349 . . . . . . . . 9 class (𝑛‘(𝑥𝑔𝑦))
13 c2 11783 . . . . . . . . 9 class 2
14 cexp 13533 . . . . . . . . 9 class
1512, 13, 14co 7182 . . . . . . . 8 class ((𝑛‘(𝑥𝑔𝑦))↑2)
16 c1 10628 . . . . . . . . . . . . 13 class 1
1716cneg 10961 . . . . . . . . . . . 12 class -1
18 vs . . . . . . . . . . . . 13 setvar 𝑠
1918cv 1541 . . . . . . . . . . . 12 class 𝑠
2017, 6, 19co 7182 . . . . . . . . . . 11 class (-1𝑠𝑦)
214, 20, 8co 7182 . . . . . . . . . 10 class (𝑥𝑔(-1𝑠𝑦))
2221, 11cfv 6349 . . . . . . . . 9 class (𝑛‘(𝑥𝑔(-1𝑠𝑦)))
2322, 13, 14co 7182 . . . . . . . 8 class ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)
24 caddc 10630 . . . . . . . 8 class +
2515, 23, 24co 7182 . . . . . . 7 class (((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2))
264, 11cfv 6349 . . . . . . . . . 10 class (𝑛𝑥)
2726, 13, 14co 7182 . . . . . . . . 9 class ((𝑛𝑥)↑2)
286, 11cfv 6349 . . . . . . . . . 10 class (𝑛𝑦)
2928, 13, 14co 7182 . . . . . . . . 9 class ((𝑛𝑦)↑2)
3027, 29, 24co 7182 . . . . . . . 8 class (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2))
31 cmul 10632 . . . . . . . 8 class ·
3213, 30, 31co 7182 . . . . . . 7 class (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))
3325, 32wceq 1542 . . . . . 6 wff (((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))
348crn 5536 . . . . . 6 class ran 𝑔
3533, 5, 34wral 3054 . . . . 5 wff 𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))
3635, 3, 34wral 3054 . . . 4 wff 𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))
3736, 7, 18, 10coprab 7183 . . 3 class {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))}
382, 37cin 3852 . 2 class (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))})
391, 38wceq 1542 1 wff CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))})
Colors of variables: wff setvar class
This definition is referenced by:  phnv  28761  isphg  28764
  Copyright terms: Public domain W3C validator