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 = BaseSet ⁡ U
imsmet.8 ⊢ D = IndMet ⁡ U
Assertion imsmet ⊢ U ∈ NrmCVec → D ∈ Met ⁡ X

Proof

Step Hyp Ref Expression
1 imsmet.1 ⊢ X = BaseSet ⁡ U
2 imsmet.8 ⊢ D = IndMet ⁡ U
3 fveq2 ⊢ U = if U ∈ NrmCVec U + × abs → IndMet ⁡ U = IndMet ⁡ if U ∈ NrmCVec U + × abs
4 fveq2 ⊢ U = if U ∈ NrmCVec U + × abs → BaseSet ⁡ U = BaseSet ⁡ if U ∈ NrmCVec U + × abs
5 1 4 syl5eq ⊢ U = if U ∈ NrmCVec U + × abs → X = BaseSet ⁡ if U ∈ NrmCVec U + × abs
6 5 fveq2d ⊢ U = if U ∈ NrmCVec U + × abs → Met ⁡ X = Met ⁡ BaseSet ⁡ if U ∈ NrmCVec U + × abs
7 3 6 eleq12d ⊢ U = if U ∈ NrmCVec U + × abs → IndMet ⁡ U ∈ Met ⁡ X ↔ IndMet ⁡ if U ∈ NrmCVec U + × abs ∈ Met ⁡ BaseSet ⁡ if U ∈ NrmCVec U + × abs
8 eqid ⊢ BaseSet ⁡ if U ∈ NrmCVec U + × abs = BaseSet ⁡ if U ∈ NrmCVec U + × abs
9 eqid ⊢ + v ⁡ if U ∈ NrmCVec U + × abs = + v ⁡ if U ∈ NrmCVec U + × abs
10 eqid ⊢ inv ⁡ + v ⁡ if U ∈ NrmCVec U + × abs = inv ⁡ + v ⁡ if U ∈ NrmCVec U + × abs
11 eqid ⊢ ⋅ 𝑠OLD ⁡ if U ∈ NrmCVec U + × abs = ⋅ 𝑠OLD ⁡ if U ∈ NrmCVec U + × abs
12 eqid ⊢ 0 vec ⁡ if U ∈ NrmCVec U + × abs = 0 vec ⁡ if U ∈ NrmCVec U + × abs
13 eqid ⊢ norm CV ⁡ if U ∈ NrmCVec U + × abs = norm CV ⁡ if U ∈ NrmCVec U + × abs
14 eqid ⊢ IndMet ⁡ if U ∈ NrmCVec U + × abs = IndMet ⁡ if U ∈ NrmCVec U + × abs
15 elimnvu ⊢ if U ∈ NrmCVec U + × abs ∈ NrmCVec
16 8 9 10 11 12 13 14 15 imsmetlem ⊢ IndMet ⁡ if U ∈ NrmCVec U + × abs ∈ Met ⁡ BaseSet ⁡ if U ∈ NrmCVec U + × abs
17 7 16 dedth ⊢ U ∈ NrmCVec → IndMet ⁡ U ∈ Met ⁡ X
18 2 17 eqeltrid ⊢ U ∈ NrmCVec → D ∈ Met ⁡ X