This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cphipeq0

Description: The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of Kreyszig p. 129. Complex version of ipeq0 . (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 cphipeq0 
|- ( ( W e. CPreHil /\ A e. V ) -> ( ( A ., A ) = 0 <-> A = .0. ) )

Proof

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