Theorem ncvsprp

Description: Proportionality property of the norm of a scalar product in a normed subcomplex vector space. (Contributed by NM, 11-Nov-2006) (Revised by AV, 8-Oct-2021)

	Ref	Expression
Hypotheses	ncvsprp.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ncvsprp.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
	ncvsprp.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	ncvsprp.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	ncvsprp.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	ncvsprp	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 · 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )

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		elin	⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec ) )
7		nvcnlm	⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod )
8	7	adantr	⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec ) → 𝑊 ∈ NrmMod )
9	6 8	sylbi	⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → 𝑊 ∈ NrmMod )
10		eqid	⊢ ( norm ‘ 𝐹 ) = ( norm ‘ 𝐹 )
11	1 2 3 4 5 10	nmvs	⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
12	9 11	syl3an1	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
13		id	⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂVec )
14	13	cvsclm	⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂMod )
15	6 14	simplbiim	⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → 𝑊 ∈ ℂMod )
16	4 5	clmabs	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( abs ‘ 𝐴 ) = ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) )
17	15 16	sylan	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝐾 ) → ( abs ‘ 𝐴 ) = ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) )
18	17	3adant3	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( abs ‘ 𝐴 ) = ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) )
19	18	eqcomd	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) = ( abs ‘ 𝐴 ) )
20	19	oveq1d	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
21	12 20	eqtrd	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 · 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )