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

Theorem phnv 28686
 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 28685 . . 3 CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))})
2 inss1 4134 . . 3 (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))}) ⊆ NrmCVec
31, 2eqsstri 3927 . 2 CPreHilOLD ⊆ NrmCVec
43sseli 3889 1 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2112  ∀wral 3071   ∩ cin 3858  ran crn 5523  ‘cfv 6333  (class class class)co 7148  {coprab 7149  1c1 10566   + caddc 10568   · cmul 10570  -cneg 10899  2c2 11719  ↑cexp 13469  NrmCVeccnv 28456  CPreHilOLDccphlo 28684 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-in 3866  df-ss 3876  df-ph 28685 This theorem is referenced by:  phrel  28687  phnvi  28688  phop  28690  isph  28694  dipdi  28715  dipassr  28718  dipsubdir  28720  dipsubdi  28721  ajval  28733  minvecolem1  28746  minvecolem2  28747  minvecolem3  28748  minvecolem4a  28749  minvecolem4b  28750  minvecolem4  28752  minvecolem5  28753  minvecolem6  28754  minvecolem7  28755
 Copyright terms: Public domain W3C validator