Metamath Proof Explorer

Theorem ipeq0

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) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f 
|- F = ( Scalar ` W )
phllmhm.h 
|- ., = ( .i ` W )
phllmhm.v 
|- V = ( Base ` W )
ip0l.z 
|- Z = ( 0g ` F )
ip0l.o 
|- .0. = ( 0g ` W )
Assertion ipeq0 
|- ( ( W e. PreHil /\ A e. V ) -> ( ( A ., A ) = Z <-> A = .0. ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f 
 |-  F = ( Scalar ` W )
2 phllmhm.h 
 |-  ., = ( .i ` W )
3 phllmhm.v 
 |-  V = ( Base ` W )
4 ip0l.z 
 |-  Z = ( 0g ` F )
5 ip0l.o 
 |-  .0. = ( 0g ` W )
6 eqid 
 |-  ( *r ` F ) = ( *r ` F )
7 3 1 2 5 6 4 isphl 
 |-  ( W e. PreHil <-> ( W e. LVec /\ F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( ( *r ` F ) ` ( x ., y ) ) = ( y ., x ) ) ) )
8 7 simp3bi 
 |-  ( W e. PreHil -> A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( ( *r ` F ) ` ( x ., y ) ) = ( y ., x ) ) )
9 simp2 
 |-  ( ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( ( *r ` F ) ` ( x ., y ) ) = ( y ., x ) ) -> ( ( x ., x ) = Z -> x = .0. ) )
10 9 ralimi 
 |-  ( A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( ( *r ` F ) ` ( x ., y ) ) = ( y ., x ) ) -> A. x e. V ( ( x ., x ) = Z -> x = .0. ) )
11 8 10 syl 
 |-  ( W e. PreHil -> A. x e. V ( ( x ., x ) = Z -> x = .0. ) )
12 oveq12 
 |-  ( ( x = A /\ x = A ) -> ( x ., x ) = ( A ., A ) )
13 12 anidms 
 |-  ( x = A -> ( x ., x ) = ( A ., A ) )
14 13 eqeq1d 
 |-  ( x = A -> ( ( x ., x ) = Z <-> ( A ., A ) = Z ) )
15 eqeq1 
 |-  ( x = A -> ( x = .0. <-> A = .0. ) )
16 14 15 imbi12d 
 |-  ( x = A -> ( ( ( x ., x ) = Z -> x = .0. ) <-> ( ( A ., A ) = Z -> A = .0. ) ) )
17 16 rspccva 
 |-  ( ( A. x e. V ( ( x ., x ) = Z -> x = .0. ) /\ A e. V ) -> ( ( A ., A ) = Z -> A = .0. ) )
18 11 17 sylan 
 |-  ( ( W e. PreHil /\ A e. V ) -> ( ( A ., A ) = Z -> A = .0. ) )
19 1 2 3 4 5 ip0l 
 |-  ( ( W e. PreHil /\ A e. V ) -> ( .0. ., A ) = Z )
20 oveq1 
 |-  ( A = .0. -> ( A ., A ) = ( .0. ., A ) )
21 20 eqeq1d 
 |-  ( A = .0. -> ( ( A ., A ) = Z <-> ( .0. ., A ) = Z ) )
22 19 21 syl5ibrcom 
 |-  ( ( W e. PreHil /\ A e. V ) -> ( A = .0. -> ( A ., A ) = Z ) )
23 18 22 impbid 
 |-  ( ( W e. PreHil /\ A e. V ) -> ( ( A ., A ) = Z <-> A = .0. ) )