Metamath Proof Explorer


Theorem ipcnval

Description: Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion ipcnval ABAB=AB+AB

Proof

Step Hyp Ref Expression
1 cjcl BB
2 remul ABAB=ABAB
3 1 2 sylan2 ABAB=ABAB
4 recj BB=B
5 4 adantl ABB=B
6 5 oveq2d ABAB=AB
7 imcj BB=B
8 7 adantl ABB=B
9 8 oveq2d ABAB=AB
10 imcl AA
11 10 recnd AA
12 imcl BB
13 12 recnd BB
14 mulneg2 ABAB=AB
15 11 13 14 syl2an ABAB=AB
16 9 15 eqtrd ABAB=AB
17 6 16 oveq12d ABABAB=ABAB
18 recl AA
19 18 recnd AA
20 recl BB
21 20 recnd BB
22 mulcl ABAB
23 19 21 22 syl2an ABAB
24 mulcl ABAB
25 11 13 24 syl2an ABAB
26 23 25 subnegd ABABAB=AB+AB
27 3 17 26 3eqtrd ABAB=AB+AB