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 = ( BaseSet ` U )
	nvs.4	|- S = ( .sOLD ` U )
	nvs.6	|- N = ( normCV ` U )
Assertion	nvsge0	|- ( ( U e. NrmCVec /\ ( A e. RR /\ 0 <_ A ) /\ B e. X ) -> ( N ` ( A S B ) ) = ( A x. ( N ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		nvs.1	|- X = ( BaseSet ` U )
2		nvs.4	|- S = ( .sOLD ` U )
3		nvs.6	|- N = ( normCV ` U )
4		recn	|- ( A e. RR -> A e. CC )
5	4	adantr	|- ( ( A e. RR /\ 0 <_ A ) -> A e. CC )
6	1 2 3	nvs	|- ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( N ` ( A S B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )
7	5 6	syl3an2	|- ( ( U e. NrmCVec /\ ( A e. RR /\ 0 <_ A ) /\ B e. X ) -> ( N ` ( A S B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )
8		absid	|- ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A )
9	8	3ad2ant2	|- ( ( U e. NrmCVec /\ ( A e. RR /\ 0 <_ A ) /\ B e. X ) -> ( abs ` A ) = A )
10	9	oveq1d	|- ( ( U e. NrmCVec /\ ( A e. RR /\ 0 <_ A ) /\ B e. X ) -> ( ( abs ` A ) x. ( N ` B ) ) = ( A x. ( N ` B ) ) )
11	7 10	eqtrd	|- ( ( U e. NrmCVec /\ ( A e. RR /\ 0 <_ A ) /\ B e. X ) -> ( N ` ( A S B ) ) = ( A x. ( N ` B ) ) )