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

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 → 𝑁 : 𝑋 ⟶ ℝ )