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 \in NrmCVec \to D \in Met (X)$

Proof

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