Theorem phnv 28593

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 28592	. . 3 ⊢ CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))})
2		inss1 4207	. . 3 ⊢ (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))}) ⊆ NrmCVec
3	1, 2	eqsstri 4003	. 2 ⊢ CPreHilOLD ⊆ NrmCVec
4	3	sseli 3965	1 ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ∀wral 3140   ∩ cin 3937  ran crn 5558  ‘cfv 6357  (class class class)co 7158  {coprab 7159  1c1 10540   + caddc 10542   · cmul 10544  -cneg 10873  2c2 11695  ↑cexp 13432  NrmCVeccnv 28363  CPreHil_OLDccphlo 28591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-ph 28592

This theorem is referenced by:  phrel  28594  phnvi  28595  phop  28597  isph  28601  dipdi  28622  dipassr  28625  dipsubdir  28627  dipsubdi  28628  ajval  28640  minvecolem1  28653  minvecolem2  28654  minvecolem3  28655  minvecolem4a  28656  minvecolem4b  28657  minvecolem4  28659  minvecolem5  28660  minvecolem6  28661  minvecolem7  28662