This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑆 𝐵 ) ) = ( 𝐴 · ( 𝑁 ‘ 𝐵 ) ) )