Metamath Proof Explorer

Theorem cphnmvs

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

Ref Expression
Hypotheses cphnmvs.v 
|- V = ( Base ` W )
cphnmvs.n 
|- N = ( norm ` W )
cphnmvs.s 
|- .x. = ( .s ` W )
cphnmvs.f 
|- F = ( Scalar ` W )
cphnmvs.k 
|- K = ( Base ` F )
Assertion cphnmvs 
|- ( ( W e. CPreHil /\ X e. K /\ Y e. V ) -> ( N ` ( X .x. Y ) ) = ( ( abs ` X ) x. ( N ` Y ) ) )

Proof

Step Hyp Ref Expression
1 cphnmvs.v 
 |-  V = ( Base ` W )
2 cphnmvs.n 
 |-  N = ( norm ` W )
3 cphnmvs.s 
 |-  .x. = ( .s ` W )
4 cphnmvs.f 
 |-  F = ( Scalar ` W )
5 cphnmvs.k 
 |-  K = ( Base ` F )
6 cphnlm 
 |-  ( W e. CPreHil -> W e. NrmMod )
7 eqid 
 |-  ( norm ` F ) = ( norm ` F )
8 1 2 3 4 5 7 nmvs 
 |-  ( ( W e. NrmMod /\ X e. K /\ Y e. V ) -> ( N ` ( X .x. Y ) ) = ( ( ( norm ` F ) ` X ) x. ( N ` Y ) ) )
9 6 8 syl3an1 
 |-  ( ( W e. CPreHil /\ X e. K /\ Y e. V ) -> ( N ` ( X .x. Y ) ) = ( ( ( norm ` F ) ` X ) x. ( N ` Y ) ) )
10 cphclm 
 |-  ( W e. CPreHil -> W e. CMod )
11 4 5 clmabs 
 |-  ( ( W e. CMod /\ X e. K ) -> ( abs ` X ) = ( ( norm ` F ) ` X ) )
12 10 11 sylan 
 |-  ( ( W e. CPreHil /\ X e. K ) -> ( abs ` X ) = ( ( norm ` F ) ` X ) )
13 12 3adant3 
 |-  ( ( W e. CPreHil /\ X e. K /\ Y e. V ) -> ( abs ` X ) = ( ( norm ` F ) ` X ) )
14 13 oveq1d 
 |-  ( ( W e. CPreHil /\ X e. K /\ Y e. V ) -> ( ( abs ` X ) x. ( N ` Y ) ) = ( ( ( norm ` F ) ` X ) x. ( N ` Y ) ) )
15 9 14 eqtr4d 
 |-  ( ( W e. CPreHil /\ X e. K /\ Y e. V ) -> ( N ` ( X .x. Y ) ) = ( ( abs ` X ) x. ( N ` Y ) ) )