Theorem phnv 31473

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ∀wral 3080   ∩ cin 4092  ran crn 5659  ‘cfv 6566  (class class class)co 7451  {coprab 7452  1c1 11240   + caddc 11242   · cmul 11244   -cneg 11581  2c2 12437  ↑cexp 14244  NrmCVeccnv 31243  CPreHil_OLDccphlo 31471

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-in 4094  df-ph 31472

This theorem is used by:  phrel  31474  phnvi  31475  phop  31477  isph  31481  dipdi  31502  dipassr  31505  dipsubdir  31507  dipsubdi  31508  ajval  31520  minvecolem1  31533  minvecolem2  31534  minvecolem3  31535  minvecolem4a  31536  minvecolem4b  31537  minvecolem4  31539  minvecolem5  31540  minvecolem6  31541  minvecolem7  31542