Theorem phnv 30743

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044   ∩ cin 3913  ran crn 5639  ‘cfv 6511  (class class class)co 7387  {coprab 7388  1c1 11069   + caddc 11071   · cmul 11073  -cneg 11406  2c2 12241  ↑cexp 14026  NrmCVeccnv 30513  CPreHil_OLDccphlo 30741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-ss 3931  df-ph 30742

This theorem is referenced by:  phrel  30744  phnvi  30745  phop  30747  isph  30751  dipdi  30772  dipassr  30775  dipsubdir  30777  dipsubdi  30778  ajval  30790  minvecolem1  30803  minvecolem2  30804  minvecolem3  30805  minvecolem4a  30806  minvecolem4b  30807  minvecolem4  30809  minvecolem5  30810  minvecolem6  30811  minvecolem7  30812