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 )