# 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 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
imsmet.8 ${⊢}{D}=\mathrm{IndMet}\left({U}\right)$
Assertion imsmet ${⊢}{U}\in \mathrm{NrmCVec}\to {D}\in \mathrm{Met}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 imsmet.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 imsmet.8 ${⊢}{D}=\mathrm{IndMet}\left({U}\right)$
3 fveq2 ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \mathrm{IndMet}\left({U}\right)=\mathrm{IndMet}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)$
4 fveq2 ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \mathrm{BaseSet}\left({U}\right)=\mathrm{BaseSet}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)$
5 1 4 syl5eq ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to {X}=\mathrm{BaseSet}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)$
6 5 fveq2d ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \mathrm{Met}\left({X}\right)=\mathrm{Met}\left(\mathrm{BaseSet}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\right)$
7 3 6 eleq12d ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \left(\mathrm{IndMet}\left({U}\right)\in \mathrm{Met}\left({X}\right)↔\mathrm{IndMet}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\in \mathrm{Met}\left(\mathrm{BaseSet}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\right)\right)$
8 eqid ${⊢}\mathrm{BaseSet}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)=\mathrm{BaseSet}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)$
9 eqid ${⊢}{+}_{v}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)={+}_{v}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)$
10 eqid ${⊢}\mathrm{inv}\left({+}_{v}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\right)=\mathrm{inv}\left({+}_{v}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\right)$
11 eqid ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)={\cdot }_{\mathrm{𝑠OLD}}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)$
12 eqid ${⊢}{0}_{\mathrm{vec}}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)={0}_{\mathrm{vec}}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)$
13 eqid ${⊢}{norm}_{CV}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)={norm}_{CV}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)$
14 eqid ${⊢}\mathrm{IndMet}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)=\mathrm{IndMet}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)$
15 elimnvu ${⊢}if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\in \mathrm{NrmCVec}$
16 8 9 10 11 12 13 14 15 imsmetlem ${⊢}\mathrm{IndMet}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\in \mathrm{Met}\left(\mathrm{BaseSet}\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\right)$
17 7 16 dedth ${⊢}{U}\in \mathrm{NrmCVec}\to \mathrm{IndMet}\left({U}\right)\in \mathrm{Met}\left({X}\right)$
18 2 17 eqeltrid ${⊢}{U}\in \mathrm{NrmCVec}\to {D}\in \mathrm{Met}\left({X}\right)$