nvnd

Description: The norm of a normed complex vector space expressed in terms of the distance function of its induced metric. Problem 1 of Kreyszig p. 63. (Contributed by NM, 4-Dec-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvnd.1	$⊢ X = BaseSet (U)$
	nvnd.5	$⊢ Z = 0_{vec} (U)$
	nvnd.6	$⊢ N = {norm}_{CV} (U)$
	nvnd.8	$⊢ D = IndMet (U)$
Assertion	nvnd	$⊢ (U \in NrmCVec \land A \in X) \to N (A) = A D Z$

Proof

Step	Hyp	Ref	Expression
1		nvnd.1	$⊢ X = BaseSet (U)$
2		nvnd.5	$⊢ Z = 0_{vec} (U)$
3		nvnd.6	$⊢ N = {norm}_{CV} (U)$
4		nvnd.8	$⊢ D = IndMet (U)$
5	1 2	nvzcl	$⊢ U \in NrmCVec \to Z \in X$
6	5	adantr	$⊢ (U \in NrmCVec \land A \in X) \to Z \in X$
7		eqid	$⊢ -_{v} (U) = -_{v} (U)$
8	1 7 3 4	imsdval	$⊢ (U \in NrmCVec \land A \in X \land Z \in X) \to A D Z = N (A -_{v} (U) Z)$
9	6 8	mpd3an3	$⊢ (U \in NrmCVec \land A \in X) \to A D Z = N (A -_{v} (U) Z)$
10		eqid	$⊢ +_{v} (U) = +_{v} (U)$
11		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
12	1 10 11 7	nvmval	$⊢ (U \in NrmCVec \land A \in X \land Z \in X) \to A -_{v} (U) Z = A +_{v} (U) (-1 \cdot_{𝑠OLD} (U) Z)$
13	6 12	mpd3an3	$⊢ (U \in NrmCVec \land A \in X) \to A -_{v} (U) Z = A +_{v} (U) (-1 \cdot_{𝑠OLD} (U) Z)$
14		neg1cn	$⊢ - 1 \in ℂ$
15	11 2	nvsz	$⊢ (U \in NrmCVec \land - 1 \in ℂ) \to -1 \cdot_{𝑠OLD} (U) Z = Z$
16	14 15	mpan2	$⊢ U \in NrmCVec \to -1 \cdot_{𝑠OLD} (U) Z = Z$
17	16	oveq2d	$⊢ U \in NrmCVec \to A +_{v} (U) (-1 \cdot_{𝑠OLD} (U) Z) = A +_{v} (U) Z$
18	17	adantr	$⊢ (U \in NrmCVec \land A \in X) \to A +_{v} (U) (-1 \cdot_{𝑠OLD} (U) Z) = A +_{v} (U) Z$
19	1 10 2	nv0rid	$⊢ (U \in NrmCVec \land A \in X) \to A +_{v} (U) Z = A$
20	13 18 19	3eqtrd	$⊢ (U \in NrmCVec \land A \in X) \to A -_{v} (U) Z = A$
21	20	fveq2d	$⊢ (U \in NrmCVec \land A \in X) \to N (A -_{v} (U) Z) = N (A)$
22	9 21	eqtr2d	$⊢ (U \in NrmCVec \land A \in X) \to N (A) = A D Z$

Metamath Proof Explorer

Theorem nvnd

Proof