This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nvcli

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

Ref Expression
Hypotheses nvf.1 ⊢ X = BaseSet ⁡ U
nvf.6 ⊢ N = norm CV ⁡ U
nvcli.9 ⊢ U ∈ NrmCVec
nvcli.7 ⊢ A ∈ X
Assertion nvcli ⊢ N ⁡ A ∈ ℝ

Proof

Step Hyp Ref Expression
1 nvf.1 ⊢ X = BaseSet ⁡ U
2 nvf.6 ⊢ N = norm CV ⁡ U
3 nvcli.9 ⊢ U ∈ NrmCVec
4 nvcli.7 ⊢ A ∈ X
5 1 2 nvcl ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ∈ ℝ
6 3 4 5 mp2an ⊢ N ⁡ A ∈ ℝ