Metamath Proof Explorer

Theorem imsdval2

Description: Value of the distance function of the induced metric of a normed complex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	imsdval2.1	$⊢ X = BaseSet (U)$
		imsdval2.2	$⊢ G = +_{v} (U)$
		imsdval2.4	$⊢ S = \cdot_{𝑠OLD} (U)$
		imsdval2.6	$⊢ N = {norm}_{CV} (U)$
		imsdval2.8	$⊢ D = IndMet (U)$
	Assertion	imsdval2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A D B = N (A G (-1 S B))$

Proof

Step	Hyp	Ref	Expression
1		imsdval2.1	$⊢ X = BaseSet (U)$
2		imsdval2.2	$⊢ G = +_{v} (U)$
3		imsdval2.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		imsdval2.6	$⊢ N = {norm}_{CV} (U)$
5		imsdval2.8	$⊢ D = IndMet (U)$
6		eqid	$⊢ -_{v} (U) = -_{v} (U)$
7	1 6 4 5	imsdval	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A D B = N (A -_{v} (U) B)$
8	1 2 3 6	nvmval	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A -_{v} (U) B = A G (-1 S B)$
9	8	fveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A -_{v} (U) B) = N (A G (-1 S B))$
10	7 9	eqtrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A D B = N (A G (-1 S B))$