Metamath Proof Explorer


Theorem cphipcj

Description: Conjugate of an inner product in a subcomplex pre-Hilbert space. Complex version of ipcj . (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses cphipcj.h ,˙=𝑖W
cphipcj.v V=BaseW
Assertion cphipcj WCPreHilAVBVA,˙B=B,˙A

Proof

Step Hyp Ref Expression
1 cphipcj.h ,˙=𝑖W
2 cphipcj.v V=BaseW
3 cphclm WCPreHilWCMod
4 eqid ScalarW=ScalarW
5 4 clmcj WCMod*=*ScalarW
6 3 5 syl WCPreHil*=*ScalarW
7 6 3ad2ant1 WCPreHilAVBV*=*ScalarW
8 7 fveq1d WCPreHilAVBVA,˙B=A,˙B*ScalarW
9 cphphl WCPreHilWPreHil
10 eqid *ScalarW=*ScalarW
11 4 1 2 10 ipcj WPreHilAVBVA,˙B*ScalarW=B,˙A
12 9 11 syl3an1 WCPreHilAVBVA,˙B*ScalarW=B,˙A
13 8 12 eqtrd WCPreHilAVBVA,˙B=B,˙A