Metamath Proof Explorer

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 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )