Theorem ipffn

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

	Ref	Expression
Hypotheses	ipffn.1	|- V = ( Base ` W )
	ipffn.2	|- ., = ( .if ` W )
Assertion	ipffn	|- ., Fn ( V X. V )

Proof

Step	Hyp	Ref	Expression
1		ipffn.1	|- V = ( Base ` W )
2		ipffn.2	|- ., = ( .if ` W )
3		eqid	|- ( .i ` W ) = ( .i ` W )
4	1 3 2	ipffval	|- ., = ( x e. V , y e. V |-> ( x ( .i ` W ) y ) )
5		ovex	|- ( x ( .i ` W ) y ) e. _V
6	4 5	fnmpoi	|- ., Fn ( V X. V )