ncvsge0

Description: The norm of a scalar product with a nonnegative real. (Contributed by NM, 1-Jan-2008) (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	ncvsge0	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in (K \cap ℝ) \land 0 \leq A) \land B \in V) \to N (A \underset{˙}{\cdot} B) = A N (B)$

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		elinel1	$⊢ A \in (K \cap ℝ) \to A \in K$
7	6	adantr	$⊢ (A \in (K \cap ℝ) \land 0 \leq A) \to A \in K$
8	1 2 3 4 5	ncvsprp	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in K \land B \in V) \to N (A \underset{˙}{\cdot} B) = \|A\| N (B)$
9	7 8	syl3an2	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in (K \cap ℝ) \land 0 \leq A) \land B \in V) \to N (A \underset{˙}{\cdot} B) = \|A\| N (B)$
10		elinel2	$⊢ A \in (K \cap ℝ) \to A \in ℝ$
11		absid	$⊢ (A \in ℝ \land 0 \leq A) \to \|A\| = A$
12	10 11	sylan	$⊢ (A \in (K \cap ℝ) \land 0 \leq A) \to \|A\| = A$
13	12	3ad2ant2	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in (K \cap ℝ) \land 0 \leq A) \land B \in V) \to \|A\| = A$
14	13	oveq1d	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in (K \cap ℝ) \land 0 \leq A) \land B \in V) \to \|A\| N (B) = A N (B)$
15	9 14	eqtrd	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in (K \cap ℝ) \land 0 \leq A) \land B \in V) \to N (A \underset{˙}{\cdot} B) = A N (B)$

Metamath Proof Explorer