Theorem phnv 30856

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2107  ∀wral 3060   ∩ cin 3963  ran crn 5691  ‘cfv 6566  (class class class)co 7435  {coprab 7436  1c1 11160   + caddc 11162   · cmul 11164  -cneg 11497  2c2 12325  ↑cexp 14105  NrmCVeccnv 30626  CPreHil_OLDccphlo 30854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1541  df-ex 1778  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-in 3971  df-ss 3981  df-ph 30855

This theorem is referenced by:  phrel  30857  phnvi  30858  phop  30860  isph  30864  dipdi  30885  dipassr  30888  dipsubdir  30890  dipsubdi  30891  ajval  30903  minvecolem1  30916  minvecolem2  30917  minvecolem3  30918  minvecolem4a  30919  minvecolem4b  30920  minvecolem4  30922  minvecolem5  30923  minvecolem6  30924  minvecolem7  30925