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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ncvsprp.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
	ncvsprp.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	ncvsprp.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	ncvsprp.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	ncvsge0	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ ( 𝐾 ∩ ℝ ) ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( 𝑁 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ncvsprp.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		ncvsprp.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
3		ncvsprp.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		ncvsprp.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5		ncvsprp.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
6		elinel1	⊢ ( 𝐴 ∈ ( 𝐾 ∩ ℝ ) → 𝐴 ∈ 𝐾 )
7	6	adantr	⊢ ( ( 𝐴 ∈ ( 𝐾 ∩ ℝ ) ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ 𝐾 )
8	1 2 3 4 5	ncvsprp	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 · 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
9	7 8	syl3an2	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ ( 𝐾 ∩ ℝ ) ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 · 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
10		elinel2	⊢ ( 𝐴 ∈ ( 𝐾 ∩ ℝ ) → 𝐴 ∈ ℝ )
11		absid	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )
12	10 11	sylan	⊢ ( ( 𝐴 ∈ ( 𝐾 ∩ ℝ ) ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )
13	12	3ad2ant2	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ ( 𝐾 ∩ ℝ ) ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑉 ) → ( abs ‘ 𝐴 ) = 𝐴 )
14	13	oveq1d	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ ( 𝐾 ∩ ℝ ) ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑉 ) → ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) = ( 𝐴 · ( 𝑁 ‘ 𝐵 ) ) )
15	9 14	eqtrd	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ ( 𝐾 ∩ ℝ ) ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( 𝑁 ‘ 𝐵 ) ) )