Theorem nvsge0

Description: The norm of a scalar product with a nonnegative real. (Contributed by NM, 1-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvs.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	nvs.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
	nvs.6	$$⊢N={norm}_{CV}\left(U\right)$$
Assertion	nvsge0	$$⊢\left(U\in \mathrm{NrmCVec}\wedge \left(A\in ℝ\wedge 0\le A\right)\wedge B\in X\right)\to N\left(ASB\right)=AN\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nvs.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		nvs.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
3		nvs.6	$$⊢N={norm}_{CV}\left(U\right)$$
4		recn	$$⊢A\in ℝ\to A\in ℂ$$
5	4	adantr	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to A\in ℂ$$
6	1 2 3	nvs	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in ℂ\wedge B\in X\right)\to N\left(ASB\right)=\left|A\right|N\left(B\right)$$
7	5 6	syl3an2	$$⊢\left(U\in \mathrm{NrmCVec}\wedge \left(A\in ℝ\wedge 0\le A\right)\wedge B\in X\right)\to N\left(ASB\right)=\left|A\right|N\left(B\right)$$
8		absid	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \left|A\right|=A$$
9	8	3ad2ant2	$$⊢\left(U\in \mathrm{NrmCVec}\wedge \left(A\in ℝ\wedge 0\le A\right)\wedge B\in X\right)\to \left|A\right|=A$$
10	9	oveq1d	$$⊢\left(U\in \mathrm{NrmCVec}\wedge \left(A\in ℝ\wedge 0\le A\right)\wedge B\in X\right)\to \left|A\right|N\left(B\right)=AN\left(B\right)$$
11	7 10	eqtrd	$$⊢\left(U\in \mathrm{NrmCVec}\wedge \left(A\in ℝ\wedge 0\le A\right)\wedge B\in X\right)\to N\left(ASB\right)=AN\left(B\right)$$