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

Metamath Proof Explorer

Theorem ipz

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. (Contributed by NM, 24-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses dip0r.1 
|- X = ( BaseSet ` U )
dip0r.5 
|- Z = ( 0vec ` U )
dip0r.7 
|- P = ( .iOLD ` U )
Assertion ipz 
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( A P A ) = 0 <-> A = Z ) )

Proof

Step Hyp Ref Expression
1 dip0r.1 
 |-  X = ( BaseSet ` U )
2 dip0r.5 
 |-  Z = ( 0vec ` U )
3 dip0r.7 
 |-  P = ( .iOLD ` U )
4 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
5 1 4 3 ipidsq 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( A P A ) = ( ( ( normCV ` U ) ` A ) ^ 2 ) )
6 5 eqeq1d 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( A P A ) = 0 <-> ( ( ( normCV ` U ) ` A ) ^ 2 ) = 0 ) )
7 1 4 nvcl 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( normCV ` U ) ` A ) e. RR )
8 7 recnd 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( normCV ` U ) ` A ) e. CC )
9 sqeq0 
 |-  ( ( ( normCV ` U ) ` A ) e. CC -> ( ( ( ( normCV ` U ) ` A ) ^ 2 ) = 0 <-> ( ( normCV ` U ) ` A ) = 0 ) )
10 8 9 syl 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( ( normCV ` U ) ` A ) ^ 2 ) = 0 <-> ( ( normCV ` U ) ` A ) = 0 ) )
11 1 2 4 nvz 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( normCV ` U ) ` A ) = 0 <-> A = Z ) )
12 6 10 11 3bitrd 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( A P A ) = 0 <-> A = Z ) )