ncvspds

Description: Value of the distance function in terms of the norm of a normed subcomplex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 28-Nov-2006) (Revised by AV, 13-Oct-2021)

	Ref	Expression
Hypotheses	ncvspds.n	$⊢ N = norm (G)$
	ncvspds.x	$⊢ X = {Base}_{G}$
	ncvspds.p	$⊢ \underset{˙}{+} = +_{G}$
	ncvspds.d	$⊢ D = dist (G)$
	ncvspds.s	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	ncvspds	$⊢ (G \in (NrmVec \cap ℂVec) \land A \in X \land B \in X) \to A D B = N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))$

Proof

Step	Hyp	Ref	Expression
1		ncvspds.n	$⊢ N = norm (G)$
2		ncvspds.x	$⊢ X = {Base}_{G}$
3		ncvspds.p	$⊢ \underset{˙}{+} = +_{G}$
4		ncvspds.d	$⊢ D = dist (G)$
5		ncvspds.s	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
6		elin	$⊢ G \in (NrmVec \cap ℂVec) \leftrightarrow (G \in NrmVec \land G \in ℂVec)$
7		nvcnlm	$⊢ G \in NrmVec \to G \in NrmMod$
8		nlmngp	$⊢ G \in NrmMod \to G \in NrmGrp$
9	7 8	syl	$⊢ G \in NrmVec \to G \in NrmGrp$
10	9	adantr	$⊢ (G \in NrmVec \land G \in ℂVec) \to G \in NrmGrp$
11	6 10	sylbi	$⊢ G \in (NrmVec \cap ℂVec) \to G \in NrmGrp$
12		eqid	$⊢ -_{G} = -_{G}$
13	1 2 12 4	ngpds	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A D B = N (A -_{G} B)$
14	11 13	syl3an1	$⊢ (G \in (NrmVec \cap ℂVec) \land A \in X \land B \in X) \to A D B = N (A -_{G} B)$
15		id	$⊢ G \in ℂVec \to G \in ℂVec$
16	15	cvsclm	$⊢ G \in ℂVec \to G \in CMod$
17	6 16	simplbiim	$⊢ G \in (NrmVec \cap ℂVec) \to G \in CMod$
18		eqid	$⊢ Scalar (G) = Scalar (G)$
19	2 3 12 18 5	clmvsubval	$⊢ (G \in CMod \land A \in X \land B \in X) \to A -_{G} B = A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)$
20	17 19	syl3an1	$⊢ (G \in (NrmVec \cap ℂVec) \land A \in X \land B \in X) \to A -_{G} B = A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)$
21	20	fveq2d	$⊢ (G \in (NrmVec \cap ℂVec) \land A \in X \land B \in X) \to N (A -_{G} B) = N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))$
22	14 21	eqtrd	$⊢ (G \in (NrmVec \cap ℂVec) \land A \in X \land B \in X) \to A D B = N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B))$

Metamath Proof Explorer

Theorem ncvspds

Proof