Theorem phnv 30800

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3052   ∩ cin 3930  ran crn 5660  ‘cfv 6536  (class class class)co 7410  {coprab 7411  1c1 11135   + caddc 11137   · cmul 11139  -cneg 11472  2c2 12300  ↑cexp 14084  NrmCVeccnv 30570  CPreHil_OLDccphlo 30798

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-in 3938  df-ss 3948  df-ph 30799

This theorem is referenced by:  phrel  30801  phnvi  30802  phop  30804  isph  30808  dipdi  30829  dipassr  30832  dipsubdir  30834  dipsubdi  30835  ajval  30847  minvecolem1  30860  minvecolem2  30861  minvecolem3  30862  minvecolem4a  30863  minvecolem4b  30864  minvecolem4  30866  minvecolem5  30867  minvecolem6  30868  minvecolem7  30869