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 ) |
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 ) |