Theorem 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	|- .x. = ( .s ` W )
	ncvsprp.f	|- F = ( Scalar ` W )
	ncvsprp.k	|- K = ( Base ` F )
Assertion	ncvsge0	|- ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. ( K i^i RR ) /\ 0 <_ A ) /\ B e. V ) -> ( N ` ( A .x. B ) ) = ( A x. ( N ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		ncvsprp.v	|- V = ( Base ` W )
2		ncvsprp.n	|- N = ( norm ` W )
3		ncvsprp.s	|- .x. = ( .s ` W )
4		ncvsprp.f	|- F = ( Scalar ` W )
5		ncvsprp.k	|- K = ( Base ` F )
6		elinel1	|- ( A e. ( K i^i RR ) -> A e. K )
7	6	adantr	|- ( ( A e. ( K i^i RR ) /\ 0 <_ A ) -> A e. K )
8	1 2 3 4 5	ncvsprp	|- ( ( W e. ( NrmVec i^i CVec ) /\ A e. K /\ B e. V ) -> ( N ` ( A .x. B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )
9	7 8	syl3an2	|- ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. ( K i^i RR ) /\ 0 <_ A ) /\ B e. V ) -> ( N ` ( A .x. B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )
10		elinel2	|- ( A e. ( K i^i RR ) -> A e. RR )
11		absid	|- ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A )
12	10 11	sylan	|- ( ( A e. ( K i^i RR ) /\ 0 <_ A ) -> ( abs ` A ) = A )
13	12	3ad2ant2	|- ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. ( K i^i RR ) /\ 0 <_ A ) /\ B e. V ) -> ( abs ` A ) = A )
14	13	oveq1d	|- ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. ( K i^i RR ) /\ 0 <_ A ) /\ B e. V ) -> ( ( abs ` A ) x. ( N ` B ) ) = ( A x. ( N ` B ) ) )
15	9 14	eqtrd	|- ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. ( K i^i RR ) /\ 0 <_ A ) /\ B e. V ) -> ( N ` ( A .x. B ) ) = ( A x. ( N ` B ) ) )