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 → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )