Theorem phlipf

Description: The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Hypotheses	ipffn.1	$$⊢V={\mathrm{Base}}_W$$
	ipffn.2	$$⊢\underset{\dot{}}{,}={\cdot }_{\mathrm{if}}\left(W\right)$$
	phlipf.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
	phlipf.k	$$⊢K={\mathrm{Base}}_S$$
Assertion	phlipf	$$⊢W\in \mathrm{PreHil}\to \underset{\dot{}}{,}:V\times V⟶K$$

Proof

Step	Hyp	Ref	Expression
1		ipffn.1	$$⊢V={\mathrm{Base}}_W$$
2		ipffn.2	$$⊢\underset{\dot{}}{,}={\cdot }_{\mathrm{if}}\left(W\right)$$
3		phlipf.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
4		phlipf.k	$$⊢K={\mathrm{Base}}_S$$
5		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
6	3 5 1 4	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge x\in V\wedge y\in V\right)\to x{\cdot }_{𝑖}\left(W\right)y\in K$$
7	6	3expb	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(x\in V\wedge y\in V\right)\right)\to x{\cdot }_{𝑖}\left(W\right)y\in K$$
8	7	ralrimivva	$$⊢W\in \mathrm{PreHil}\to \forall x\in V\forall y\in Vx{\cdot }_{𝑖}\left(W\right)y\in K$$
9	1 5 2	ipffval	$$⊢\underset{\dot{}}{,}=\left(x\in V,y\in V⟼x{\cdot }_{𝑖}\left(W\right)y\right)$$
10	9	fmpo	$$⊢\forall x\in V\forall y\in Vx{\cdot }_{𝑖}\left(W\right)y\in K\leftrightarrow \underset{\dot{}}{,}:V\times V⟶K$$
11	8 10	sylib	$$⊢W\in \mathrm{PreHil}\to \underset{\dot{}}{,}:V\times V⟶K$$