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	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
Assertion	cphipcj	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to \overline{A\underset{\dot{}}{,}B}=B\underset{\dot{}}{,}A$$

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
2		cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
3		cphclm	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{CMod}$$
4		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
5	4	clmcj	$$⊢W\in \mathrm{CMod}\to *={\mathrm{*}}_{\mathrm{Scalar}\left(W\right)}$$
6	3 5	syl	$$⊢W\in \mathrm{CPreHil}\to *={\mathrm{*}}_{\mathrm{Scalar}\left(W\right)}$$
7	6	3ad2ant1	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to *={\mathrm{*}}_{\mathrm{Scalar}\left(W\right)}$$
8	7	fveq1d	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to \overline{A\underset{\dot{}}{,}B}={\left(A\underset{\dot{}}{,}B\right)}^{{\mathrm{*}}_{\mathrm{Scalar}\left(W\right)}}$$
9		cphphl	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{PreHil}$$
10		eqid	$$⊢{\mathrm{*}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{*}}_{\mathrm{Scalar}\left(W\right)}$$
11	4 1 2 10	ipcj	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to {\left(A\underset{\dot{}}{,}B\right)}^{{\mathrm{*}}_{\mathrm{Scalar}\left(W\right)}}=B\underset{\dot{}}{,}A$$
12	9 11	syl3an1	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to {\left(A\underset{\dot{}}{,}B\right)}^{{\mathrm{*}}_{\mathrm{Scalar}\left(W\right)}}=B\underset{\dot{}}{,}A$$
13	8 12	eqtrd	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to \overline{A\underset{\dot{}}{,}B}=B\underset{\dot{}}{,}A$$