Theorem ipcl

Description: Closure of the inner product operation in a pre-Hilbert space. (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$$
	ipcl.f	$$⊢K={\mathrm{Base}}_F$$
Assertion	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{,}B\in K$$

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		ipcl.f	$$⊢K={\mathrm{Base}}_F$$
5		eqid	$$⊢\left(x\in V⟼x\underset{\dot{}}{,}B\right)=\left(x\in V⟼x\underset{\dot{}}{,}B\right)$$
6	1 2 3 5	phllmhm	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\right)\to \left(x\in V⟼x\underset{\dot{}}{,}B\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)$$
7		rlmbas	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{ringLMod}\left(F\right)}$$
8	4 7	eqtri	$$⊢K={\mathrm{Base}}_{\mathrm{ringLMod}\left(F\right)}$$
9	3 8	lmhmf	$$⊢\left(x\in V⟼x\underset{\dot{}}{,}B\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\to \left(x\in V⟼x\underset{\dot{}}{,}B\right):V⟶K$$
10	6 9	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\right)\to \left(x\in V⟼x\underset{\dot{}}{,}B\right):V⟶K$$
11	5	fmpt	$$⊢\forall x\in Vx\underset{\dot{}}{,}B\in K\leftrightarrow \left(x\in V⟼x\underset{\dot{}}{,}B\right):V⟶K$$
12	10 11	sylibr	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\right)\to \forall x\in Vx\underset{\dot{}}{,}B\in K$$
13		oveq1	$$⊢x=A\to x\underset{\dot{}}{,}B=A\underset{\dot{}}{,}B$$
14	13	eleq1d	$$⊢x=A\to \left(x\underset{\dot{}}{,}B\in K\leftrightarrow A\underset{\dot{}}{,}B\in K\right)$$
15	14	rspccva	$$⊢\left(\forall x\in Vx\underset{\dot{}}{,}B\in K\wedge A\in V\right)\to A\underset{\dot{}}{,}B\in K$$
16	12 15	stoic3	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\wedge A\in V\right)\to A\underset{\dot{}}{,}B\in K$$
17	16	3com23	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{,}B\in K$$