Metamath Proof Explorer


Theorem cphip0r

Description: Inner product with a zero second argument. Complex version of ip0r . (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses cphipcj.h
|- ., = ( .i ` W )
cphipcj.v
|- V = ( Base ` W )
cphip0l.z
|- .0. = ( 0g ` W )
Assertion cphip0r
|- ( ( W e. CPreHil /\ A e. V ) -> ( A ., .0. ) = 0 )

Proof

Step Hyp Ref Expression
1 cphipcj.h
 |-  ., = ( .i ` W )
2 cphipcj.v
 |-  V = ( Base ` W )
3 cphip0l.z
 |-  .0. = ( 0g ` W )
4 cphphl
 |-  ( W e. CPreHil -> W e. PreHil )
5 eqid
 |-  ( Scalar ` W ) = ( Scalar ` W )
6 eqid
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
7 5 1 2 6 3 ip0r
 |-  ( ( W e. PreHil /\ A e. V ) -> ( A ., .0. ) = ( 0g ` ( Scalar ` W ) ) )
8 4 7 sylan
 |-  ( ( W e. CPreHil /\ A e. V ) -> ( A ., .0. ) = ( 0g ` ( Scalar ` W ) ) )
9 cphclm
 |-  ( W e. CPreHil -> W e. CMod )
10 5 clm0
 |-  ( W e. CMod -> 0 = ( 0g ` ( Scalar ` W ) ) )
11 9 10 syl
 |-  ( W e. CPreHil -> 0 = ( 0g ` ( Scalar ` W ) ) )
12 11 adantr
 |-  ( ( W e. CPreHil /\ A e. V ) -> 0 = ( 0g ` ( Scalar ` W ) ) )
13 8 12 eqtr4d
 |-  ( ( W e. CPreHil /\ A e. V ) -> ( A ., .0. ) = 0 )