Theorem imsxmet

Description: The induced metric of a normed complex vector space is an extended metric space. (Contributed by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	imsmet.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	imsmet.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion	imsxmet	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		imsmet.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		imsmet.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3	1 2	imsmet	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( Met ‘ 𝑋 ) )
4		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
5	3 4	syl	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )