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 ⊢ X = BaseSet ⁡ U
nvf.6 ⊢ N = norm CV ⁡ U
Assertion nvf ⊢ U ∈ NrmCVec → N : X ⟶ ℝ

Proof

Step Hyp Ref Expression
1 nvf.1 ⊢ X = BaseSet ⁡ U
2 nvf.6 ⊢ N = norm CV ⁡ U
3 eqid ⊢ + v ⁡ U = + v ⁡ U
4 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
5 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
6 1 3 4 5 2 nvi ⊢ U ∈ NrmCVec → + v ⁡ U ⋅ 𝑠OLD ⁡ U ∈ CVec OLD ∧ N : X ⟶ ℝ ∧ ∀ x ∈ X N ⁡ x = 0 → x = 0 vec ⁡ U ∧ ∀ y ∈ ℂ N ⁡ y ⋅ 𝑠OLD ⁡ U x = y ⁢ N ⁡ x ∧ ∀ y ∈ X N ⁡ x + v ⁡ U y ≤ N ⁡ x + N ⁡ y
7 6 simp2d ⊢ U ∈ NrmCVec → N : X ⟶ ℝ