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

Theorem phnv 28518
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 28517 . . 3 CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))})
2 inss1 4202 . . 3 (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))}) ⊆ NrmCVec
31, 2eqsstri 3998 . 2 CPreHilOLD ⊆ NrmCVec
43sseli 3960 1 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  wral 3135  cin 3932  ran crn 5549  cfv 6348  (class class class)co 7145  {coprab 7146  1c1 10526   + caddc 10528   · cmul 10530  -cneg 10859  2c2 11680  cexp 13417  NrmCVeccnv 28288  CPreHilOLDccphlo 28516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-in 3940  df-ss 3949  df-ph 28517
This theorem is referenced by:  phrel  28519  phnvi  28520  phop  28522  isph  28526  dipdi  28547  dipassr  28550  dipsubdir  28552  dipsubdi  28553  ajval  28565  minvecolem1  28578  minvecolem2  28579  minvecolem3  28580  minvecolem4a  28581  minvecolem4b  28582  minvecolem4  28584  minvecolem5  28585  minvecolem6  28586  minvecolem7  28587
  Copyright terms: Public domain W3C validator