This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )