ncvsprp

Description: Proportionality property of the norm of a scalar product in a normed subcomplex vector space. (Contributed by NM, 11-Nov-2006) (Revised by AV, 8-Oct-2021)

	Ref	Expression
Hypotheses	ncvsprp.v	$⊢ V = {Base}_{W}$
	ncvsprp.n	$⊢ N = norm (W)$
	ncvsprp.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	ncvsprp.f	$⊢ F = Scalar (W)$
	ncvsprp.k	$⊢ K = {Base}_{F}$
Assertion	ncvsprp	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in K \land B \in V) \to N (A \underset{˙}{\cdot} B) = \|A\| N (B)$

Proof

Step	Hyp	Ref	Expression
1		ncvsprp.v	$⊢ V = {Base}_{W}$
2		ncvsprp.n	$⊢ N = norm (W)$
3		ncvsprp.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		ncvsprp.f	$⊢ F = Scalar (W)$
5		ncvsprp.k	$⊢ K = {Base}_{F}$
6		elin	$⊢ W \in (NrmVec \cap ℂVec) \leftrightarrow (W \in NrmVec \land W \in ℂVec)$
7		nvcnlm	$⊢ W \in NrmVec \to W \in NrmMod$
8	7	adantr	$⊢ (W \in NrmVec \land W \in ℂVec) \to W \in NrmMod$
9	6 8	sylbi	$⊢ W \in (NrmVec \cap ℂVec) \to W \in NrmMod$
10		eqid	$⊢ norm (F) = norm (F)$
11	1 2 3 4 5 10	nmvs	$⊢ (W \in NrmMod \land A \in K \land B \in V) \to N (A \underset{˙}{\cdot} B) = norm (F) (A) N (B)$
12	9 11	syl3an1	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in K \land B \in V) \to N (A \underset{˙}{\cdot} B) = norm (F) (A) N (B)$
13		id	$⊢ W \in ℂVec \to W \in ℂVec$
14	13	cvsclm	$⊢ W \in ℂVec \to W \in CMod$
15	6 14	simplbiim	$⊢ W \in (NrmVec \cap ℂVec) \to W \in CMod$
16	4 5	clmabs	$⊢ (W \in CMod \land A \in K) \to \|A\| = norm (F) (A)$
17	15 16	sylan	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in K) \to \|A\| = norm (F) (A)$
18	17	3adant3	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in K \land B \in V) \to \|A\| = norm (F) (A)$
19	18	eqcomd	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in K \land B \in V) \to norm (F) (A) = \|A\|$
20	19	oveq1d	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in K \land B \in V) \to norm (F) (A) N (B) = \|A\| N (B)$
21	12 20	eqtrd	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in K \land B \in V) \to N (A \underset{˙}{\cdot} B) = \|A\| N (B)$

Metamath Proof Explorer

Theorem ncvsprp

Proof