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

Theorem phnv 27999
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 27998 . . 3 CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))})
2 inss1 3976 . . 3 (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛𝑥)↑2) + ((𝑛𝑦)↑2)))}) ⊆ NrmCVec
31, 2eqsstri 3776 . 2 CPreHilOLD ⊆ NrmCVec
43sseli 3740 1 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  wral 3050  cin 3714  ran crn 5267  cfv 6049  (class class class)co 6814  {coprab 6815  1c1 10149   + caddc 10151   · cmul 10153  -cneg 10479  2c2 11282  cexp 13074  NrmCVeccnv 27769  CPreHilOLDccphlo 27997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-ss 3729  df-ph 27998
This theorem is referenced by:  phrel  28000  phnvi  28001  phop  28003  isph  28007  dipdi  28028  dipassr  28031  dipsubdir  28033  dipsubdi  28034  sspph  28040  ajval  28047  minvecolem1  28060  minvecolem2  28061  minvecolem3  28062  minvecolem4a  28063  minvecolem4b  28064  minvecolem4  28066  minvecolem5  28067  minvecolem6  28068  minvecolem7  28069
  Copyright terms: Public domain W3C validator