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 = Base W
Assertion cphipcj W CPreHil A V B V A , ˙ B = B , ˙ A

Proof

Step Hyp Ref Expression
1 cphipcj.h , ˙ = 𝑖 W
2 cphipcj.v V = Base W
3 cphclm W CPreHil W CMod
4 eqid Scalar W = Scalar W
5 4 clmcj W CMod * = * Scalar W
6 3 5 syl W CPreHil * = * Scalar W
7 6 3ad2ant1 W CPreHil A V B V * = * Scalar W
8 7 fveq1d W CPreHil A V B V A , ˙ B = A , ˙ B * Scalar W
9 cphphl W CPreHil W PreHil
10 eqid * Scalar W = * Scalar W
11 4 1 2 10 ipcj W PreHil A V B V A , ˙ B * Scalar W = B , ˙ A
12 9 11 syl3an1 W CPreHil A V B V A , ˙ B * Scalar W = B , ˙ A
13 8 12 eqtrd W CPreHil A V B V A , ˙ B = B , ˙ A