Theorem ipffn

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

	Ref	Expression
Hypotheses	ipffn.1	$$⊢V={\mathrm{Base}}_W$$
	ipffn.2	$$⊢\underset{\dot{}}{,}={\cdot }_{\mathrm{if}}\left(W\right)$$
Assertion	ipffn	$$⊢\underset{\dot{}}{,}Fn\left(V\times V\right)$$

Proof

Step	Hyp	Ref	Expression
1		ipffn.1	$$⊢V={\mathrm{Base}}_W$$
2		ipffn.2	$$⊢\underset{\dot{}}{,}={\cdot }_{\mathrm{if}}\left(W\right)$$
3		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
4	1 3 2	ipffval	$$⊢\underset{\dot{}}{,}=\left(x\in V,y\in V⟼x{\cdot }_{𝑖}\left(W\right)y\right)$$
5		ovex	$$⊢x{\cdot }_{𝑖}\left(W\right)y\in \mathrm{V}$$
6	4 5	fnmpoi	$$⊢\underset{\dot{}}{,}Fn\left(V\times V\right)$$