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 | |
|
cphipcj.v | |
||
cphip0l.z | |
||
Assertion | cphipeq0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cphipcj.h | |
|
2 | cphipcj.v | |
|
3 | cphip0l.z | |
|
4 | cphclm | |
|
5 | eqid | |
|
6 | 5 | clm0 | |
7 | 4 6 | syl | |
8 | 7 | adantr | |
9 | 8 | eqeq2d | |
10 | cphphl | |
|
11 | eqid | |
|
12 | 5 1 2 11 3 | ipeq0 | |
13 | 10 12 | sylan | |
14 | 9 13 | bitrd | |