Metamath Proof Explorer


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 )