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

Theorem phnv 28125
Description: Every complex inner product space is a normed complex vector space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.)
Assertion
Ref Expression
phnv (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)

Proof of Theorem phnv
Dummy variables 𝑔 𝑛 𝑠 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ph 28124 . . 3 CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))})
2 inss1 3992 . . 3 (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))}) ⊆ NrmCVec
31, 2eqsstri 3795 . 2 CPreHilOLD ⊆ NrmCVec
43sseli 3757 1 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wcel 2155  wral 3055  cin 3731  ran crn 5278  cfv 6068  (class class class)co 6842  {coprab 6843  1c1 10190   + caddc 10192   · cmul 10194  -cneg 10521  2c2 11327  cexp 13067  NrmCVeccnv 27895  CPreHilOLDccphlo 28123
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-in 3739  df-ss 3746  df-ph 28124
This theorem is referenced by:  phrel  28126  phnvi  28127  phop  28129  isph  28133  dipdi  28154  dipassr  28157  dipsubdir  28159  dipsubdi  28160  sspphOLD  28166  ajval  28173  minvecolem1  28186  minvecolem2  28187  minvecolem3  28188  minvecolem4a  28189  minvecolem4b  28190  minvecolem4  28192  minvecolem5  28193  minvecolem6  28194  minvecolem7  28195
  Copyright terms: Public domain W3C validator