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 ⊢ X = BaseSet ⁡ U
nvs.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
nvs.6 ⊢ N = norm CV ⁡ U
Assertion nvsge0 ⊢ U ∈ NrmCVec ∧ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ X → N ⁡ A S B = A ⁢ N ⁡ B

Proof

Step Hyp Ref Expression
1 nvs.1 ⊢ X = BaseSet ⁡ U
2 nvs.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
3 nvs.6 ⊢ N = norm CV ⁡ U
4 recn ⊢ A ∈ ℝ → A ∈ ℂ
5 4 adantr ⊢ A ∈ ℝ ∧ 0 ≤ A → A ∈ ℂ
6 1 2 3 nvs ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X → N ⁡ A S B = A ⁢ N ⁡ B
7 5 6 syl3an2 ⊢ U ∈ NrmCVec ∧ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ X → N ⁡ A S B = A ⁢ N ⁡ B
8 absid ⊢ A ∈ ℝ ∧ 0 ≤ A → A = A
9 8 3ad2ant2 ⊢ U ∈ NrmCVec ∧ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ X → A = A
10 9 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ X → A ⁢ N ⁡ B = A ⁢ N ⁡ B
11 7 10 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ X → N ⁡ A S B = A ⁢ N ⁡ B