Metamath Proof Explorer


Theorem nvf

Description: Mapping for the norm function. (Contributed by NM, 11-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvf.1 𝑋 = ( BaseSet ‘ 𝑈 )
nvf.6 𝑁 = ( normCV𝑈 )
Assertion nvf ( 𝑈 ∈ NrmCVec → 𝑁 : 𝑋 ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 nvf.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvf.6 𝑁 = ( normCV𝑈 )
3 eqid ( +𝑣𝑈 ) = ( +𝑣𝑈 )
4 eqid ( ·𝑠OLD𝑈 ) = ( ·𝑠OLD𝑈 )
5 eqid ( 0vec𝑈 ) = ( 0vec𝑈 )
6 1 3 4 5 2 nvi ( 𝑈 ∈ NrmCVec → ( ⟨ ( +𝑣𝑈 ) , ( ·𝑠OLD𝑈 ) ⟩ ∈ CVecOLD𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥𝑋 ( ( ( 𝑁𝑥 ) = 0 → 𝑥 = ( 0vec𝑈 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 ( ·𝑠OLD𝑈 ) 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁𝑥 ) ) ∧ ∀ 𝑦𝑋 ( 𝑁 ‘ ( 𝑥 ( +𝑣𝑈 ) 𝑦 ) ) ≤ ( ( 𝑁𝑥 ) + ( 𝑁𝑦 ) ) ) ) )
7 6 simp2d ( 𝑈 ∈ NrmCVec → 𝑁 : 𝑋 ⟶ ℝ )