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