Metamath Proof Explorer

Theorem imsdval

Description: Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 27-Dec-2014) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	imsdval.1	$⊢ X = BaseSet (U)$
		imsdval.3	$⊢ M = -_{v} (U)$
		imsdval.6	$⊢ N = {norm}_{CV} (U)$
		imsdval.8	$⊢ D = IndMet (U)$
	Assertion	imsdval	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A D B = N (A M B)$

Proof

Step	Hyp	Ref	Expression
1		imsdval.1	$⊢ X = BaseSet (U)$
2		imsdval.3	$⊢ M = -_{v} (U)$
3		imsdval.6	$⊢ N = {norm}_{CV} (U)$
4		imsdval.8	$⊢ D = IndMet (U)$
5	2 3 4	imsval	$⊢ U \in NrmCVec \to D = N \circ M$
6	5	3ad2ant1	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to D = N \circ M$
7	6	fveq1d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to D (⟨A, B⟩) = (N \circ M) (⟨A, B⟩)$
8	1 2	nvmf	$⊢ U \in NrmCVec \to M : X \times X ⟶ X$
9		opelxpi	$⊢ (A \in X \land B \in X) \to ⟨A, B⟩ \in (X \times X)$
10		fvco3	$⊢ (M : X \times X ⟶ X \land ⟨A, B⟩ \in (X \times X)) \to (N \circ M) (⟨A, B⟩) = N (M (⟨A, B⟩))$
11	8 9 10	syl2an	$⊢ (U \in NrmCVec \land (A \in X \land B \in X)) \to (N \circ M) (⟨A, B⟩) = N (M (⟨A, B⟩))$
12	11	3impb	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (N \circ M) (⟨A, B⟩) = N (M (⟨A, B⟩))$
13	7 12	eqtrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to D (⟨A, B⟩) = N (M (⟨A, B⟩))$
14		df-ov	$⊢ A D B = D (⟨A, B⟩)$
15		df-ov	$⊢ A M B = M (⟨A, B⟩)$
16	15	fveq2i	$⊢ N (A M B) = N (M (⟨A, B⟩))$
17	13 14 16	3eqtr4g	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A D B = N (A M B)$