# 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 syl5eq ( 𝑈 = 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 ( 0vec ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( 0vec ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
13 eqid ( normCV ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( normCV ‘ 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 ‘ 𝑋 ) )