Metamath Proof Explorer

Theorem imsmet

Description: The induced metric of a normed complex vector space is a metric space. Part of Definition 2.2-1 of Kreyszig p. 58. (Contributed by NM, 4-Dec-2006) (Revised by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		imsmet.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		imsmet.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3		fveq2	⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( IndMet ‘ 𝑈 ) = ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
4		fveq2	⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
5	1 4	eqtrid	⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝑋 = ( BaseSet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
6	5	fveq2d	⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( Met ‘ 𝑋 ) = ( Met ‘ ( BaseSet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) )
7	3 6	eleq12d	⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( IndMet ‘ 𝑈 ) ∈ ( Met ‘ 𝑋 ) ↔ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∈ ( Met ‘ ( BaseSet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) ) )
8		eqid	⊢ ( BaseSet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( BaseSet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
9		eqid	⊢ ( +_𝑣 ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( +_𝑣 ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
10		eqid	⊢ ( inv ‘ ( +_𝑣 ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) = ( inv ‘ ( +_𝑣 ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
11		eqid	⊢ ( ·_𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( ·_𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
12		eqid	⊢ ( 0_vec ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( 0_vec ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
13		eqid	⊢ ( norm_CV ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( norm_CV ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
14		eqid	⊢ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
15		elimnvu	⊢ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∈ NrmCVec
16	8 9 10 11 12 13 14 15	imsmetlem	⊢ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∈ ( Met ‘ ( BaseSet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
17	7 16	dedth	⊢ ( 𝑈 ∈ NrmCVec → ( IndMet ‘ 𝑈 ) ∈ ( Met ‘ 𝑋 ) )
18	2 17	eqeltrid	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( Met ‘ 𝑋 ) )