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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nvs.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
	nvs.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion	nvsge0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( 𝐴 · ( 𝑁 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nvs.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvs.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
3		nvs.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
4		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
5	4	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℂ )
6	1 2 3	nvs	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
7	5 6	syl3an2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
8		absid	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )
9	8	3ad2ant2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ 𝐴 ) = 𝐴 )
10	9	oveq1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑋 ) → ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) = ( 𝐴 · ( 𝑁 ‘ 𝐵 ) ) )
11	7 10	eqtrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( 𝐴 · ( 𝑁 ‘ 𝐵 ) ) )