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 ,˙=𝑖W
cphipcj.v V=BaseW
cphip0l.z 0˙=0W
Assertion cphipeq0 WCPreHilAVA,˙A=0A=0˙

Proof

Step Hyp Ref Expression
1 cphipcj.h ,˙=𝑖W
2 cphipcj.v V=BaseW
3 cphip0l.z 0˙=0W
4 cphclm WCPreHilWCMod
5 eqid ScalarW=ScalarW
6 5 clm0 WCMod0=0ScalarW
7 4 6 syl WCPreHil0=0ScalarW
8 7 adantr WCPreHilAV0=0ScalarW
9 8 eqeq2d WCPreHilAVA,˙A=0A,˙A=0ScalarW
10 cphphl WCPreHilWPreHil
11 eqid 0ScalarW=0ScalarW
12 5 1 2 11 3 ipeq0 WPreHilAVA,˙A=0ScalarWA=0˙
13 10 12 sylan WCPreHilAVA,˙A=0ScalarWA=0˙
14 9 13 bitrd WCPreHilAVA,˙A=0A=0˙