Theorem phllmhm

Description: The inner product of a pre-Hilbert space is linear in its left argument. (Contributed 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$$
	phllmhm.g	$$⊢G=\left(x\in V⟼x\underset{\dot{}}{,}A\right)$$
Assertion	phllmhm	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to G\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)$$

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		phllmhm.g	$$⊢G=\left(x\in V⟼x\underset{\dot{}}{,}A\right)$$
5		eqid	$$⊢0_W=0_W$$
6		eqid	$$⊢{\mathrm{*}}_F={\mathrm{*}}_F$$
7		eqid	$$⊢0_F=0_F$$
8	3 1 2 5 6 7	isphl	$$⊢W\in \mathrm{PreHil}\leftrightarrow \left(W\in \mathrm{LVec}\wedge F\in \mathrm{*-Ring}\wedge \forall y\in V\left(\left(x\in V⟼x\underset{\dot{}}{,}y\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge \left(y\underset{\dot{}}{,}y=0_F\to y=0_W\right)\wedge \forall x\in V{\left(y\underset{\dot{}}{,}x\right)}^{{\mathrm{*}}_F}=x\underset{\dot{}}{,}y\right)\right)$$
9	8	simp3bi	$$⊢W\in \mathrm{PreHil}\to \forall y\in V\left(\left(x\in V⟼x\underset{\dot{}}{,}y\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge \left(y\underset{\dot{}}{,}y=0_F\to y=0_W\right)\wedge \forall x\in V{\left(y\underset{\dot{}}{,}x\right)}^{{\mathrm{*}}_F}=x\underset{\dot{}}{,}y\right)$$
10		simp1	$$⊢\left(\left(x\in V⟼x\underset{\dot{}}{,}y\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge \left(y\underset{\dot{}}{,}y=0_F\to y=0_W\right)\wedge \forall x\in V{\left(y\underset{\dot{}}{,}x\right)}^{{\mathrm{*}}_F}=x\underset{\dot{}}{,}y\right)\to \left(x\in V⟼x\underset{\dot{}}{,}y\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)$$
11	10	ralimi	$$⊢\forall y\in V\left(\left(x\in V⟼x\underset{\dot{}}{,}y\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge \left(y\underset{\dot{}}{,}y=0_F\to y=0_W\right)\wedge \forall x\in V{\left(y\underset{\dot{}}{,}x\right)}^{{\mathrm{*}}_F}=x\underset{\dot{}}{,}y\right)\to \forall y\in V\left(x\in V⟼x\underset{\dot{}}{,}y\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)$$
12	9 11	syl	$$⊢W\in \mathrm{PreHil}\to \forall y\in V\left(x\in V⟼x\underset{\dot{}}{,}y\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)$$
13		oveq2	$$⊢y=A\to x\underset{\dot{}}{,}y=x\underset{\dot{}}{,}A$$
14	13	mpteq2dv	$$⊢y=A\to \left(x\in V⟼x\underset{\dot{}}{,}y\right)=\left(x\in V⟼x\underset{\dot{}}{,}A\right)$$
15	14 4	eqtr4di	$$⊢y=A\to \left(x\in V⟼x\underset{\dot{}}{,}y\right)=G$$
16	15	eleq1d	$$⊢y=A\to \left(\left(x\in V⟼x\underset{\dot{}}{,}y\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\leftrightarrow G\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\right)$$
17	16	rspccva	$$⊢\left(\forall y\in V\left(x\in V⟼x\underset{\dot{}}{,}y\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge A\in V\right)\to G\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)$$
18	12 17	sylan	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to G\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)$$