Metamath Proof Explorer


Theorem phlipf

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

Ref Expression
Hypotheses ipffn.1
|- V = ( Base ` W )
ipffn.2
|- ., = ( .if ` W )
phlipf.s
|- S = ( Scalar ` W )
phlipf.k
|- K = ( Base ` S )
Assertion phlipf
|- ( W e. PreHil -> ., : ( V X. V ) --> K )

Proof

Step Hyp Ref Expression
1 ipffn.1
 |-  V = ( Base ` W )
2 ipffn.2
 |-  ., = ( .if ` W )
3 phlipf.s
 |-  S = ( Scalar ` W )
4 phlipf.k
 |-  K = ( Base ` S )
5 eqid
 |-  ( .i ` W ) = ( .i ` W )
6 3 5 1 4 ipcl
 |-  ( ( W e. PreHil /\ x e. V /\ y e. V ) -> ( x ( .i ` W ) y ) e. K )
7 6 3expb
 |-  ( ( W e. PreHil /\ ( x e. V /\ y e. V ) ) -> ( x ( .i ` W ) y ) e. K )
8 7 ralrimivva
 |-  ( W e. PreHil -> A. x e. V A. y e. V ( x ( .i ` W ) y ) e. K )
9 1 5 2 ipffval
 |-  ., = ( x e. V , y e. V |-> ( x ( .i ` W ) y ) )
10 9 fmpo
 |-  ( A. x e. V A. y e. V ( x ( .i ` W ) y ) e. K <-> ., : ( V X. V ) --> K )
11 8 10 sylib
 |-  ( W e. PreHil -> ., : ( V X. V ) --> K )