Theorem nvcl 8227

Description: The norm of a normed complex vector space is a real number.

Hypotheses

Ref	Expression
nvf.1	|- X = (Base` U)
nvf.6	|- N = (norm` U)

Assertion

Ref	Expression
nvcl	|- ((U e. NrmCVec /\ A e. X) -> (N` A) e. RR)

Proof of Theorem nvcl

Step	Hyp	Ref	Expression
1		ffvelrn 3799	. 2 |- ((N:X-->RR /\ A e. X) -> (N` A) e. RR)
2		nvf.1	. . 3 |- X = (Base` U)
3		nvf.6	. . 3 |- N = (norm` U)
4	2, 3	nvf 8226	. 2 |- (U e. NrmCVec -> N:X-->RR)
5	1, 4	sylan 448	1 |- ((U e. NrmCVec /\ A e. X) -> (N` A) e. RR)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 953   e. wcel 955  -->wf 3168  ` cfv 3172  RRcr 5205  NrmCVeccnv 8141  Basecba 8143  normcnm 8147

This theorem is referenced by:  nvcli 8228  nvm1 8231  nvpi 8233  nvz0 8235  nvmtri 8238  nvabs 8240  nvge0 8241  nvgt0 8242  nv1 8243  nmcnilem 8272  ipval2lem2 8288  4ipval2 8292  ipval2lem5 8294  ipid 8297  ipnm 8298  ipz 8306  ip1cnilem3 8309  ip1cnilem5 8311  ip1cnilem6 8312  nmosetre 8359  nmoge0 8362  nmoub3i 8368  nmounbi 8371  nmlno0lem 8385  nmblolbii 8390  blocnilem 8395  ipblnfi 8447  ubthlem5 8464  ubthlem7 8466  ubthlem8 8467  ubthlem9 8468  ubthlem10 8469  ubthlem11 8470  ubthlem12 8471  minveclem5 8480  minveclem9 8484  minveclem10 8485  minveclem14 8489  minveclem16 8491  minveclem18 8493  minveclem20 8495  minveclem21 8496  minveclem22 8497  minveclem27 8502  minveclem28 8503  minveclem30 8505  minveclem31 8506  minveclem36 8511  minveclem38 8513  minveceu 8514  hlipgt0 8546  htthlem6 8555  htthlem7 8556  htthlem8 8557  htthlem9 8558  htthlem10 8559  htthlem12 8561

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-rab 1644  df-v 1803  df-sbc 1932  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-id 2824  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-fo 3186  df-fv 3188  df-opr 3950  df-oprab 3951  df-1st 4063  df-2nd 4064  df-grp 7971  df-gid 7972  df-nv 8149  df-va 8152  df-ba 8153  df-sm 8154  df-0v 8155  df-nm 8157

Copyright terms: Public domain