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

Metamath Proof Explorer

Theorem imsdf

Description: Mapping for the induced metric distance function of a normed complex vector space. (Contributed by NM, 29-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses imsdfn.1 ⊢ X = BaseSet ⁡ U
imsdfn.8 ⊢ D = IndMet ⁡ U
Assertion imsdf ⊢ U ∈ NrmCVec → D : X × X ⟶ ℝ

Proof

Step Hyp Ref Expression
1 imsdfn.1 ⊢ X = BaseSet ⁡ U
2 imsdfn.8 ⊢ D = IndMet ⁡ U
3 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
4 1 3 nvf ⊢ U ∈ NrmCVec → norm CV ⁡ U : X ⟶ ℝ
5 eqid ⊢ - v ⁡ U = - v ⁡ U
6 1 5 nvmf ⊢ U ∈ NrmCVec → - v ⁡ U : X × X ⟶ X
7 fco ⊢ norm CV ⁡ U : X ⟶ ℝ ∧ - v ⁡ U : X × X ⟶ X → norm CV ⁡ U ∘ - v ⁡ U : X × X ⟶ ℝ
8 4 6 7 syl2anc ⊢ U ∈ NrmCVec → norm CV ⁡ U ∘ - v ⁡ U : X × X ⟶ ℝ
9 5 3 2 imsval ⊢ U ∈ NrmCVec → D = norm CV ⁡ U ∘ - v ⁡ U
10 9 feq1d ⊢ U ∈ NrmCVec → D : X × X ⟶ ℝ ↔ norm CV ⁡ U ∘ - v ⁡ U : X × X ⟶ ℝ
11 8 10 mpbird ⊢ U ∈ NrmCVec → D : X × X ⟶ ℝ