Theorem nvcl 30597

Description: The norm of a normed complex vector space is a real number. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.)

Hypotheses

Ref	Expression
nvf.1	⊢ 𝑋 = (BaseSet‘𝑈)
nvf.6	⊢ 𝑁 = (normCV‘𝑈)

Assertion

Ref	Expression
nvcl	⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ)

Proof of Theorem nvcl

Step	Hyp	Ref	Expression
1		nvf.1	. . 3 ⊢ 𝑋 = (BaseSet‘𝑈)
2		nvf.6	. . 3 ⊢ 𝑁 = (normCV‘𝑈)
3	1, 2	nvf 30596	. 2 ⊢ (𝑈 ∈ NrmCVec → 𝑁:𝑋⟶ℝ)
4	3	ffvelcdmda 7059	1 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  ℝcr 11074  NrmCVeccnv 30520  BaseSetcba 30522  norm_CVcnmcv 30526

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-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-1st 7971  df-2nd 7972  df-vc 30495  df-nv 30528  df-va 30531  df-ba 30532  df-sm 30533  df-0v 30534  df-nmcv 30536

This theorem is referenced by:  nvcli  30598  nvm1  30601  nvpi  30603  nvz0  30604  nvmtri  30607  nvabs  30608  nvge0  30609  nvgt0  30610  nv1  30611  nmcvcn  30631  smcnlem  30633  ipval2lem2  30640  4ipval2  30644  ipidsq  30646  ipnm  30647  ipz  30655  nmosetre  30700  nmooge0  30703  nmoub3i  30709  nmounbi  30712  nmlno0lem  30729  nmblolbii  30735  blocnilem  30740  ipblnfi  30791  ubthlem1  30806  ubthlem2  30807  ubthlem3  30808  minvecolem1  30810  minvecolem2  30811  minvecolem4  30816  minvecolem5  30817  minvecolem6  30818  hlipgt0  30850  htthlem  30853