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.

Step	Hyp	Ref	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
3	1, 2	eqsstri 3927	. 2 ⊢ CPreHilOLD ⊆ NrmCVec
4	3	sseli 3889	1 ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec)

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  CPreHil_OLDccphlo 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