Description: Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999) (Revised by Mario Carneiro, 14-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | ipcnval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cjcl | |
|
2 | remul | |
|
3 | 1 2 | sylan2 | |
4 | recj | |
|
5 | 4 | adantl | |
6 | 5 | oveq2d | |
7 | imcj | |
|
8 | 7 | adantl | |
9 | 8 | oveq2d | |
10 | imcl | |
|
11 | 10 | recnd | |
12 | imcl | |
|
13 | 12 | recnd | |
14 | mulneg2 | |
|
15 | 11 13 14 | syl2an | |
16 | 9 15 | eqtrd | |
17 | 6 16 | oveq12d | |
18 | recl | |
|
19 | 18 | recnd | |
20 | recl | |
|
21 | 20 | recnd | |
22 | mulcl | |
|
23 | 19 21 22 | syl2an | |
24 | mulcl | |
|
25 | 11 13 24 | syl2an | |
26 | 23 25 | subnegd | |
27 | 3 17 26 | 3eqtrd | |