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=\mathrm{Scalar}\left(W\right)$$
	phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
	ipcj.i	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_F$$
Assertion	ipcj	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \underset{\dot{}}{\ast }\left(A\underset{\dot{}}{,}B\right)=B\underset{\dot{}}{,}A$$

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
4		ipcj.i	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_F$$
5		eqid	$$⊢0_W=0_W$$
6		eqid	$$⊢0_F=0_F$$
7	3 1 2 5 4 6	isphl	$$⊢W\in \mathrm{PreHil}\leftrightarrow \left(W\in \mathrm{LVec}\wedge F\in \mathrm{*-Ring}\wedge \forall x\in V\left(\left(y\in V⟼y\underset{\dot{}}{,}x\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge \left(x\underset{\dot{}}{,}x=0_F\to x=0_W\right)\wedge \forall y\in V\underset{\dot{}}{\ast }\left(x\underset{\dot{}}{,}y\right)=y\underset{\dot{}}{,}x\right)\right)$$
8	7	simp3bi	$$⊢W\in \mathrm{PreHil}\to \forall x\in V\left(\left(y\in V⟼y\underset{\dot{}}{,}x\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge \left(x\underset{\dot{}}{,}x=0_F\to x=0_W\right)\wedge \forall y\in V\underset{\dot{}}{\ast }\left(x\underset{\dot{}}{,}y\right)=y\underset{\dot{}}{,}x\right)$$
9		simp3	$$⊢\left(\left(y\in V⟼y\underset{\dot{}}{,}x\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge \left(x\underset{\dot{}}{,}x=0_F\to x=0_W\right)\wedge \forall y\in V\underset{\dot{}}{\ast }\left(x\underset{\dot{}}{,}y\right)=y\underset{\dot{}}{,}x\right)\to \forall y\in V\underset{\dot{}}{\ast }\left(x\underset{\dot{}}{,}y\right)=y\underset{\dot{}}{,}x$$
10	9	ralimi	$$⊢\forall x\in V\left(\left(y\in V⟼y\underset{\dot{}}{,}x\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge \left(x\underset{\dot{}}{,}x=0_F\to x=0_W\right)\wedge \forall y\in V\underset{\dot{}}{\ast }\left(x\underset{\dot{}}{,}y\right)=y\underset{\dot{}}{,}x\right)\to \forall x\in V\forall y\in V\underset{\dot{}}{\ast }\left(x\underset{\dot{}}{,}y\right)=y\underset{\dot{}}{,}x$$
11	8 10	syl	$$⊢W\in \mathrm{PreHil}\to \forall x\in V\forall y\in V\underset{\dot{}}{\ast }\left(x\underset{\dot{}}{,}y\right)=y\underset{\dot{}}{,}x$$
12		fvoveq1	$$⊢x=A\to \underset{\dot{}}{\ast }\left(x\underset{\dot{}}{,}y\right)=\underset{\dot{}}{\ast }\left(A\underset{\dot{}}{,}y\right)$$
13		oveq2	$$⊢x=A\to y\underset{\dot{}}{,}x=y\underset{\dot{}}{,}A$$
14	12 13	eqeq12d	$$⊢x=A\to \left(\underset{\dot{}}{\ast }\left(x\underset{\dot{}}{,}y\right)=y\underset{\dot{}}{,}x\leftrightarrow \underset{\dot{}}{\ast }\left(A\underset{\dot{}}{,}y\right)=y\underset{\dot{}}{,}A\right)$$
15		oveq2	$$⊢y=B\to A\underset{\dot{}}{,}y=A\underset{\dot{}}{,}B$$
16	15	fveq2d	$$⊢y=B\to \underset{\dot{}}{\ast }\left(A\underset{\dot{}}{,}y\right)=\underset{\dot{}}{\ast }\left(A\underset{\dot{}}{,}B\right)$$
17		oveq1	$$⊢y=B\to y\underset{\dot{}}{,}A=B\underset{\dot{}}{,}A$$
18	16 17	eqeq12d	$$⊢y=B\to \left(\underset{\dot{}}{\ast }\left(A\underset{\dot{}}{,}y\right)=y\underset{\dot{}}{,}A\leftrightarrow \underset{\dot{}}{\ast }\left(A\underset{\dot{}}{,}B\right)=B\underset{\dot{}}{,}A\right)$$
19	14 18	rspc2v	$$⊢\left(A\in V\wedge B\in V\right)\to \left(\forall x\in V\forall y\in V\underset{\dot{}}{\ast }\left(x\underset{\dot{}}{,}y\right)=y\underset{\dot{}}{,}x\to \underset{\dot{}}{\ast }\left(A\underset{\dot{}}{,}B\right)=B\underset{\dot{}}{,}A\right)$$
20	11 19	syl5com	$$⊢W\in \mathrm{PreHil}\to \left(\left(A\in V\wedge B\in V\right)\to \underset{\dot{}}{\ast }\left(A\underset{\dot{}}{,}B\right)=B\underset{\dot{}}{,}A\right)$$
21	20	3impib	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \underset{\dot{}}{\ast }\left(A\underset{\dot{}}{,}B\right)=B\underset{\dot{}}{,}A$$