Metamath Proof Explorer

Theorem cphnmvs

Description: Norm of a scalar product. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses cphnmvs.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
cphnmvs.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
cphnmvs.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
cphnmvs.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cphnmvs.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion cphnmvs ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( ( abs ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 cphnmvs.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 cphnmvs.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
3 cphnmvs.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 cphnmvs.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5 cphnmvs.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
6 cphnlm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod )
7 eqid ⊢ ( norm ‘ 𝐹 ) = ( norm ‘ 𝐹 )
8 1 2 3 4 5 7 nmvs ⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )
9 6 8 syl3an1 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )
10 cphclm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
11 4 5 clmabs ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ) → ( abs ‘ 𝑋 ) = ( ( norm ‘ 𝐹 ) ‘ 𝑋 ) )
12 10 11 sylan ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝐾 ) → ( abs ‘ 𝑋 ) = ( ( norm ‘ 𝐹 ) ‘ 𝑋 ) )
13 12 3adant3 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( abs ‘ 𝑋 ) = ( ( norm ‘ 𝐹 ) ‘ 𝑋 ) )
14 13 oveq1d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( ( abs ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )
15 9 14 eqtr4d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( ( abs ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )