Metamath Proof Explorer


Theorem ipcj

Description: Conjugate of an inner product in a pre-Hilbert space. Equation I1 of Ponnusamy p. 362. (Contributed by NM, 1-Feb-2007) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f F=ScalarW
phllmhm.h ,˙=𝑖W
phllmhm.v V=BaseW
ipcj.i ˙=*F
Assertion ipcj WPreHilAVBV˙A,˙B=B,˙A

Proof

Step Hyp Ref Expression
1 phlsrng.f F=ScalarW
2 phllmhm.h ,˙=𝑖W
3 phllmhm.v V=BaseW
4 ipcj.i ˙=*F
5 eqid 0W=0W
6 eqid 0F=0F
7 3 1 2 5 4 6 isphl WPreHilWLVecF*-RingxVyVy,˙xWLMHomringLModFx,˙x=0Fx=0WyV˙x,˙y=y,˙x
8 7 simp3bi WPreHilxVyVy,˙xWLMHomringLModFx,˙x=0Fx=0WyV˙x,˙y=y,˙x
9 simp3 yVy,˙xWLMHomringLModFx,˙x=0Fx=0WyV˙x,˙y=y,˙xyV˙x,˙y=y,˙x
10 9 ralimi xVyVy,˙xWLMHomringLModFx,˙x=0Fx=0WyV˙x,˙y=y,˙xxVyV˙x,˙y=y,˙x
11 8 10 syl WPreHilxVyV˙x,˙y=y,˙x
12 fvoveq1 x=A˙x,˙y=˙A,˙y
13 oveq2 x=Ay,˙x=y,˙A
14 12 13 eqeq12d x=A˙x,˙y=y,˙x˙A,˙y=y,˙A
15 oveq2 y=BA,˙y=A,˙B
16 15 fveq2d y=B˙A,˙y=˙A,˙B
17 oveq1 y=By,˙A=B,˙A
18 16 17 eqeq12d y=B˙A,˙y=y,˙A˙A,˙B=B,˙A
19 14 18 rspc2v AVBVxVyV˙x,˙y=y,˙x˙A,˙B=B,˙A
20 11 19 syl5com WPreHilAVBV˙A,˙B=B,˙A
21 20 3impib WPreHilAVBV˙A,˙B=B,˙A