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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
imsdfn.8 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion imsdf ( 𝑈 ∈ NrmCVec → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 imsdfn.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 imsdfn.8 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3 eqid ⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
4 1 3 nvf ⊢ ( 𝑈 ∈ NrmCVec → ( normCV ‘ 𝑈 ) : 𝑋 ⟶ ℝ )
5 eqid ⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 )
6 1 5 nvmf ⊢ ( 𝑈 ∈ NrmCVec → ( −𝑣 ‘ 𝑈 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
7 fco ⊢ ( ( ( normCV ‘ 𝑈 ) : 𝑋 ⟶ ℝ ∧ ( −𝑣 ‘ 𝑈 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
8 4 6 7 syl2anc ⊢ ( 𝑈 ∈ NrmCVec → ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
9 5 3 2 imsval ⊢ ( 𝑈 ∈ NrmCVec → 𝐷 = ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) )
10 9 feq1d ⊢ ( 𝑈 ∈ NrmCVec → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ↔ ( ( normCV ‘ 𝑈 ) ∘ ( −𝑣 ‘ 𝑈 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ) )
11 8 10 mpbird ⊢ ( 𝑈 ∈ NrmCVec → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )