Metamath Proof Explorer


Theorem ipcni

Description: Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999)

Ref Expression
Hypotheses recl.1 A
readdi.2 B
Assertion ipcni AB=AB+AB

Proof

Step Hyp Ref Expression
1 recl.1 A
2 readdi.2 B
3 ipcnval ABAB=AB+AB
4 1 2 3 mp2an AB=AB+AB