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 ) )